OAI/Geometry/NodalSets/Charts/PositiveMetric.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.Geometry.positive_metric_injective line 13
2. lemma OAI.Yau.Geometry.dual_continuous_finrank line 25
3. def OAI.Yau.Geometry.positiveMetricEquiv line 29
4. lemma OAI.Yau.Geometry.positiveMetricEquiv_apply line 34
5. theorem OAI.Yau.Geometry.positive_metric_connection line 38