Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Todo @ 423:9984cdd88da3
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Aug 2020 18:05:23 +0900 |
parents | bca043423554 |
children | f4dac8be0a01 |
line wrap: on
line diff
--- a/Todo Sat Aug 01 11:06:29 2020 +0900 +++ b/Todo Sat Aug 01 18:05:23 2020 +0900 @@ -1,6 +1,12 @@ +Sat Aug 1 13:16:53 JST 2020 + + P Generic Filter + as a ZF model + define Definition for L + Tue Jul 23 11:02:50 JST 2019 - define cardinals + define cardinals ... done prove CH in OD→ZF define Ultra filter ... done define L M : ZF ZFSet = M is an OD