OAI/Geometry/TamingCompatibility/DifferentialForms/PositiveFunctions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.positiveFunctions line 27
2. lemma OAI.TamingCompatibility.convex_positiveFunctions line 30
3. lemma OAI.TamingCompatibility.isOpen_positiveFunctions line 39
4. theorem OAI.TamingCompatibility.exists_normalized_positive_annihilator line 52
5. theorem OAI.TamingCompatibility.exists_probability_annihilating_subspace line 93
6. lemma OAI.TamingCompatibility.IsSmooth.continuous_tangentEval line 126
7. abbrev OAI.TamingCompatibility.MetricUnit line 139
8. lemma OAI.TamingCompatibility.isCompact_metricUnit line 143
9. instance OAI.TamingCompatibility.(instance at line 163) line 163
10. def OAI.TamingCompatibility.unitEvaluation line 168