OAI/Geometry/Relativity/CKS/CKSTensorCompact.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSMixedGeometry.tensorRegion_open line 13
2. lemma OAI.CKSMixedGeometry.tensorRegion_zero line 17
3. lemma OAI.CKSMixedGeometry.tensor_family_bound line 23
4. def OAI.CKSMixedGeometry.boundedTensorFamily line 51
5. lemma OAI.CKSMixedGeometry.boundedTensorFamily_compact line 54
6. theorem OAI.CKSMixedGeometry.cks_tensor_coefficients_bounded line 60