OAI/Geometry/Relativity/CKS/InducedMetric.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSInducedArea.bilinearTriv_baseSet line 44
2. lemma OAI.CKSInducedArea.bilinearTriv_pair line 47
3. lemma OAI.CKSInducedArea.bilinearComp_smoothAt line 81
4. lemma OAI.CKSInducedArea.inducedInner_smooth line 98
5. lemma OAI.CKSInducedArea.positive_bilinear_bounded line 126
6. lemma OAI.CKSInducedArea.inducedInner_symm line 168
7. lemma OAI.CKSInducedArea.inducedInner_pos line 174
8. lemma OAI.CKSInducedArea.inducedInner_bounded line 182
9. lemma OAI.CKSInducedArea.inducedMetric_lower line 189