OAI/GroupTheory/SimpleAmenable/CentralCovers/PrimitiveFormalSectors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.starFamily_projection line 23
2. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.formalSector_projection line 40
3. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.formalSector_subfamily_eq line 59
4. theorem OAI.SimpleAmenable.resolvedPartitionSelector line 111
5. theorem OAI.SimpleAmenable.FormalStarTable.sector_empty line 144
6. theorem OAI.SimpleAmenable.FormalStarTable.sector_range_le_biUnion line 150
7. theorem OAI.SimpleAmenable.FormalStarTable.sector_range_le_partition line 180