OAI/Geometry/TamingCompatibility/Charts/ChartLift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.ManifoldForms.chartLift line 14
2. def OAI.TamingCompatibility.ManifoldForms.liftSupport line 20
3. lemma OAI.TamingCompatibility.ManifoldForms.liftSupport_subset line 24
4. lemma OAI.TamingCompatibility.ManifoldForms.liftSupport_compact line 31
5. lemma OAI.TamingCompatibility.ManifoldForms.chartLift_zero_off line 37
6. lemma OAI.TamingCompatibility.ManifoldForms.pullback_chartLift line 49
7. lemma OAI.TamingCompatibility.ManifoldForms.chartLift_smooth line 63