OAI/SetTheory/PartitionPrinciple/Geometry/GroundCompressionMarkingRecognition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_compressionBases line 20
2. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_compressionCaps line 31
3. def OAI.PartitionPilot.Forcing.TransitiveGround.compressionBasesFormula line 42
4. def OAI.PartitionPilot.Forcing.TransitiveGround.compressionCapsFormula line 47
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_compressionBasesFormula line 52
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_compressionCapsFormula line 66
7. theorem OAI.PartitionPilot.Forcing.GroundCompressionAlgebra.realize_basesFormula line 91
8. theorem OAI.PartitionPilot.Forcing.GroundCompressionAlgebra.realize_capsFormula line 100