OAI/Geometry/NodalSets/Charts/CompactFrameCover.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Yau.Geometry.CompactFrameCover line 13
2. def OAI.Yau.Geometry.CompactFrameCover.Parameter line 25
3. instance OAI.Yau.Geometry.CompactFrameCover.(instance at line 26) line 26
4. instance OAI.Yau.Geometry.CompactFrameCover.(instance at line 27) line 27
5. def OAI.Yau.Geometry.CompactFrameCover.center line 30
6. lemma OAI.Yau.Geometry.CompactFrameCover.continuous_center line 31
7. lemma OAI.Yau.Geometry.CompactFrameCover.surjective_center line 35
8. def OAI.Yau.Geometry.CompactFrameCover.triple line 40
9. theorem OAI.Yau.Geometry.exists_compact_frame_cover line 54