OAI/Geometry/Relativity/CKS/BoundarySmooth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSBoundarySurface.ext_symm_lift line 16
2. lemma OAI.CKSBoundarySurface.lift_mem_ext_target line 21
3. lemma OAI.CKSBoundarySurface.transition_lift_maps line 28
4. lemma OAI.CKSBoundarySurface.transition_formula line 41
5. lemma OAI.CKSBoundarySurface.inclusion_chart_formula line 50
6. lemma OAI.CKSBoundarySurface.inclusion_chart_eventually line 57
7. lemma OAI.CKSBoundarySurface.inclusion_smooth line 64
8. lemma OAI.CKSBoundarySurface.inclusion_hasMFDeriv line 70
9. lemma OAI.CKSBoundarySurface.inclusion_mfderiv_injective line 75