OAI/Geometry/Relativity/CKS/BoundaryPlane.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CKSIntrinsicGeometry.E3 line 9
2. def OAI.CKSIntrinsicGeometry.boundaryPlane line 10
3. lemma OAI.CKSIntrinsicGeometry.boundaryPlane_finrank line 13
4. lemma OAI.CKSIntrinsicGeometry.boundary_plane_ball_area_finite line 24