diff Todo @ 338:bca043423554

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Jul 2020 12:32:42 +0900
parents ac872f6b8692
children 9984cdd88da3
line wrap: on
line diff
--- a/Todo	Tue Jul 07 15:32:11 2020 +0900
+++ b/Todo	Sun Jul 12 12:32:42 2020 +0900
@@ -2,7 +2,7 @@
 
     define cardinals 
     prove CH in OD→ZF
-    define Ultra filter
+    define Ultra filter  ... done
     define L M : ZF ZFSet = M is an OD
     define L N : ZF ZFSet = N = G M (G is a generic fitler on M )
     prove ¬ CH on L N
@@ -10,7 +10,7 @@
 
 Mon Jul  8 19:43:37 JST 2019
 
-    ordinal-definable.agda assumes all ZF Set are ordinals, that it too restrictive
+    ordinal-definable.agda assumes all ZF Set are ordinals, that it too restrictive  ... fixed
 
     remove ord-Ord  and prove with some assuption in HOD.agda
         union, power set, replace, inifinite