OAI/SetTheory/PartitionPrinciple/Geometry/RootedSupportOrder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.supports_lower line 12
2. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.leastSupport_depth_mono line 17
3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.leastSupport_eq_of_depth_eq line 22
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.supports_coordinate_unique line 31
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.leastSupport_iff_not_parent line 36
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RootedGluing.Scheme.leastSupport_coordinates line 49