OAI/Topology/ArtinGroups/Realizations/CellInteriorChart.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.sourceCellInteriorChart line 14
2. lemma OAI.HarmonicArtin.sourceCellTotal_restrict_ball line 33
3. lemma OAI.HarmonicArtin.sourceCellTotal_embedding_ball line 40
4. lemma OAI.HarmonicArtin.sourceCellTotal_injOn_ball line 46
5. def OAI.HarmonicArtin.sourceCellPartial line 53
6. lemma OAI.HarmonicArtin.sourceCellPartial_source line 57
7. lemma OAI.HarmonicArtin.sourceCellPartial_apply line 60
8. lemma OAI.HarmonicArtin.sourceCellPartial_continuousOn_symm line 63
9. lemma OAI.HarmonicArtin.sourceCellPartial_image_closedBall line 67
10. lemma OAI.HarmonicArtin.sourceCellPartial_image_ball line 71
11. lemma OAI.HarmonicArtin.sourceCellPartial_boundary line 75