OAI/SetTheory/PartitionPrinciple/Geometry/GroundCertificateBasisUnions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.certificateBasisGraph line 12
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateBasisGraph_function line 21
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_certificateBasisGraph line 29
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateBasisGraph_mem line 54
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateUsedSupports_eq_basisUnion line 71
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.certificateUsedSupports_ground_countable line 89