Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff Todo @ 1458:171c3f3cdc6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 26 Aug 2023 08:37:08 +0900
parents f4dac8be0a01
children e8c166541c86
line wrap: on
line diff
--- a/Todo	Sat Jul 08 08:56:01 2023 +0900
+++ b/Todo	Sat Aug 26 08:37:08 2023 +0900
@@ -1,3 +1,8 @@
+Sun Jul  9 09:42:20 JST 2023
+
+    Assume countable dense OD in Ordinal as L
+    if Power ω ∩ L is cardinal, ω c< (Power ω ∩ L) c< Power ω 
+
 Sat May 13 10:51:35 JST 2023
 
     use Filter (ZFP (Proj1 (ZFP PQ)) (Proj2 (ZFP PQ)) for projection of Ultra filter
@@ -6,12 +11,15 @@
 Sat Aug  1 13:16:53 JST 2020
 
     P Generic Filter
-        as a ZF model 
-    define Definition for L
+        as a ZF model   ( -- this is no good )
+    define Definition for L  ( -- this is no good )
 
 Tue Jul 23 11:02:50 JST 2019
 
     define cardinals     ... done
+
+    scheme on CH is no good in HOD
+
     prove CH in OD→ZF
     define Ultra filter  ... done
     define L M : ZF ZFSet = M is an OD