OAI/SetTheory/PartitionPrinciple/Geometry/GroundRefinementCoarseVisibility.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementCoarseImage_mem line 21
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementCoarseImage_principal_support line 37
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.coarseClass_visible_of_fineValue line 50
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementQuotientMap_preserves_visibility line 83