OAI/Topology/ArtinGroups/Realizations/CellIndex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.SourceCellIndex line 12
2. lemma OAI.HarmonicArtin.sourceCell_ball_pair line 14
3. def OAI.HarmonicArtin.sourceCellCoordinates line 35
4. lemma OAI.HarmonicArtin.sourceCellCoordinates_spec line 38
5. def OAI.HarmonicArtin.sourceCellBallHomeomorph line 44
6. lemma OAI.HarmonicArtin.sourceCellBallHomeomorph_apply line 50
7. lemma OAI.HarmonicArtin.sourceCellBallHomeomorph_interior_iff line 54
8. lemma OAI.HarmonicArtin.sourceCellBallHomeomorph_frontier_iff line 61
9. def OAI.HarmonicArtin.sourceCellTotal line 68
10. lemma OAI.HarmonicArtin.sourceCellTotal_closedBall line 74
11. lemma OAI.HarmonicArtin.sourceCellTotal_continuousOn line 79
12. lemma OAI.HarmonicArtin.sourceCellTotal_image_closedBall line 89
13. lemma OAI.HarmonicArtin.sourceCellTotal_image_ball line 100