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

comparison Todo @ 423:9984cdd88da3

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, 01 Aug 2020 18:05:23 +0900
parents bca043423554
children f4dac8be0a01
comparison
equal deleted inserted replaced
422:44a484f17f26 423:9984cdd88da3
1 Sat Aug 1 13:16:53 JST 2020
2
3 P Generic Filter
4 as a ZF model
5 define Definition for L
6
1 Tue Jul 23 11:02:50 JST 2019 7 Tue Jul 23 11:02:50 JST 2019
2 8
3 define cardinals 9 define cardinals ... done
4 prove CH in OD→ZF 10 prove CH in OD→ZF
5 define Ultra filter ... done 11 define Ultra filter ... done
6 define L M : ZF ZFSet = M is an OD 12 define L M : ZF ZFSet = M is an OD
7 define L N : ZF ZFSet = N = G M (G is a generic fitler on M ) 13 define L N : ZF ZFSet = N = G M (G is a generic fitler on M )
8 prove ¬ CH on L N 14 prove ¬ CH on L N