OAI/SetTheory/PartitionPrinciple/Geometry/MainInitial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initialOrder line 12
2. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initialHeight line 22
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initialHeight_countable line 34
4. def OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initial line 38
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initial_two_points line 53
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initial_bottom_ne_top line 59
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initial_action_trivial line 64
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.MainStage.initial_group_trivial line 67