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

comparison Todo @ 1283:f4dac8be0a01

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, 13 May 2023 10:53:32 +0900
parents 9984cdd88da3
children 171c3f3cdc6b
comparison
equal deleted inserted replaced
1282:dc5aaf39f27d 1283:f4dac8be0a01
1 Sat May 13 10:51:35 JST 2023
2
3 use Filter (ZFP (Proj1 (ZFP PQ)) (Proj2 (ZFP PQ)) for projection of Ultra filter
4 tranfinite induciton on well-founded set
5
1 Sat Aug 1 13:16:53 JST 2020 6 Sat Aug 1 13:16:53 JST 2020
2 7
3 P Generic Filter 8 P Generic Filter
4 as a ZF model 9 as a ZF model
5 define Definition for L 10 define Definition for L