The full parent body as a hyperspace point

noncomputable def NRR.BodySpace.parentAt (K : Geometry.ConvexBody Geometry.Plane) {A : ℝ} (hAK : A ≤ K.area) : BodySpace K A

The parent body itself, regarded as an element of BodySpace K A whenever the threshold is at most the parent's area.

Equations

• NRR.BodySpace.parentAt K hAK = ⟨⟨K.toMathlib, ⋯⟩, hAK⟩

theorem NRR.BodySpace.parentAt_body_carrier (K : Geometry.ConvexBody Geometry.Plane) {A : ℝ} (hAK : A ≤ K.area) : ↑(parentAt K hAK).body.body = K.carrier

@[simp]

theorem NRR.BodySpace.parentAt_body_area (K : Geometry.ConvexBody Geometry.Plane) {A : ℝ} (hAK : A ≤ K.area) : (parentAt K hAK).body.area = K.area

noncomputable def NRR.BodySpace.full (K : Geometry.ConvexBody Geometry.Plane) : BodySpace K K.area

The parent body itself, regarded as an element of BodySpace K K.area.

Equations

• NRR.BodySpace.full K = NRR.BodySpace.parentAt K ⋯

theorem NRR.BodySpace.full_body_carrier (K : Geometry.ConvexBody Geometry.Plane) : ↑(full K).body.body = K.carrier

@[simp]

theorem NRR.BodySpace.full_body_area (K : Geometry.ConvexBody Geometry.Plane) : (full K).body.area = K.area

theorem NRR.BodySpace.toGeometryConvexBody_full (K : Geometry.ConvexBody Geometry.Plane) (hK : 0 < K.area) : (full K).toGeometryConvexBody hK = K

The positive-area solid bridge of the full hyperspace point is the original body.