OAI/Geometry/PeriodicTiling/ConstituentAssembly.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.translated_parts_unique_ae line 16
2. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.indexed_constituents_ae line 34
3. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.center_injective line 61
4. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.center_mem_A_iff line 83
5. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.constituent_type_eq line 99
6. theorem OAI.PeriodicTilingThree.MarkedTile.ResidueSection.typed_constituents line 112
7. theorem OAI.PeriodicTilingThree.MarkedTile.period_centers line 140
8. theorem OAI.PeriodicTilingThree.MarkedTile.fullyPeriodic_centers line 158
9. theorem OAI.PeriodicTilingThree.MarkedTile.tiles_of_centers_grid line 163