Set-Theory:ZFC的Coq编码和课本集理论的形式化
需积分: 12 119 浏览量
2021-04-22
15:02:43
上传
评论
收藏 317KB ZIP 举报
Set-Theory-master.zip （79个子文件） 
Set-Theory-master 
EST8_3.v 34KB EST3_1.v 21KB _CoqProject 9B EST6_5.v 15KB EST5_7.v 49KB EST3_2.v 24KB EST4_1.v 18KB EST4_2.v 21KB ZFC2.v 11KB EST5_4.v 27KB ZFC1.v 11KB EST7_4.v 28KB EX3_1.v 19KB EX6_3.v 33KB build_all.sh 3KB build_natural.sh 997B EX7_1.v 22KB EX4.v 29KB EX7_3.v 16KB EST5_5.v 33KB EST5_2.v 26KB EST6_4.v 33KB EST8_1.v 27KB lib Dominate.v 7KB Cardinal.v 7KB misc.v 2KB FuncFacts.v 36KB ZornsLemma.v 33KB NatIsomorphism.v 3KB Natural.v 8KB EpsilonInduction.v 3KB Essential.v 370B WosetMin.v 8KB Choice.v 28KB Real.v 2KB Relation.v 93B Ordinal.v 6KB IndexedFamilyUnion.v 894B NaturalFacts.v 10KB LoStruct.v 2KB TopologicalSpace.v 2KB algebra Inj_2n3m.v 4KB OrdFacts.v 7KB Class.v 2KB ScottsTrick.v 6KB EST5_1.v 25KB EX7_2.v 20KB EST5_6.v 42KB README.zh-CN.md 3KB build_ord.sh 2KB ZFC0.v 11KB EX3_2.v 17KB EX2.v 15KB EX6_1.v 8KB EST6_2.v 51KB LICENSE 1KB EX6_2.v 12KB EST6_1.v 30KB EX8_1.v 17KB build_real.sh 528B EST7_2.v 26KB README.md 4KB ZFC3.v 3KB EX5.v 11KB EST5_3.v 29KB EST2.v 15KB EST8_2.v 12KB EST7_5.v 17KB EX8_2.v 52KB EST6_6.v 35KB EST3_3.v 10KB EST6_3.v 22KB EST7_6.v 22KB .gitignore 705B build_ord2.sh 385B EST4_3.v 16KB EST7_3.v 34KB EST7_1.v 23KB EST8_4.v 30KB资源评论
