OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalCutoffCoherence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.heightOrderRestriction_restrict line 11
2. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_order_restriction line 35
3. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_meet_restriction line 39
4. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_birth_restriction line 47
5. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.cutoff_height_restriction line 51
6. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.pair_mem_order_iff_cutoff line 64
7. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.pair_mem_meet_iff_cutoff line 78
8. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.pair_mem_birth_iff_cutoff line 94
9. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.pair_mem_height_iff_cutoff line 104