OAI/Geometry/Relativity/CKS/Transfer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSMain.restrictConstraintChart line 15
2. def OAI.CKSMain.BoundaryGeometry.transfer line 33
3. lemma OAI.CKSMain.weakBoundary_of_marginal_near line 46
4. lemma OAI.CKSMain.compact_boundary_neighbourhood line 56
5. lemma OAI.CKSMain.tail_zero_symbol line 74
6. lemma OAI.CKSMain.bondiMass_pos line 81
7. theorem OAI.CKSMain.transfer_inequality line 88