OAI/Geometry/CAT0Fillings/Gradient/ClosedLinear.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.exists_inverse_coordinates line 16
2. lemma OAI.CAT0Fillings.ChartGeometry.ae_coordinate_density_pos line 44
3. lemma OAI.CAT0Fillings.ChartGeometry.ae_multiplicity_ne_zero line 49
4. lemma OAI.CAT0Fillings.ChartGeometry.eq_zero_of_pairing_null line 69
5. theorem OAI.CAT0Fillings.ChartGeometry.gradient_closable line 109
6. lemma OAI.CAT0Fillings.ChartGeometry.gradient_add line 131
7. lemma OAI.CAT0Fillings.ChartGeometry.gradient_smul line 165
8. def OAI.CAT0Fillings.ChartGeometry.value line 192
9. lemma OAI.CAT0Fillings.ChartGeometry.value_add line 196
10. lemma OAI.CAT0Fillings.ChartGeometry.value_smul line 203
11. lemma OAI.CAT0Fillings.ChartGeometry.norm_value line 209