NRR.ConvexSubbody — fixed-parent convex subbodies

This module introduces the fixed-parent hyperspace element type

NRR.ConvexSubbody (K : Geometry.ConvexBody Plane)

whose elements are compact, nonempty, convex Mathlib bodies (_root_.ConvexBody Plane) contained in the solid parent body K. Unlike the solid geometry body Geometry.ConvexBody, a ConvexSubbody may be lower-dimensional (degenerate), which is exactly what is needed for a compact hyperspace under the Hausdorff metric.

The area of a subbody is the real-valued Lebesgue measure of its carrier, matching the convention of Geometry.ConvexBody.area.

def NRR.ConvexSubbody (K : Geometry.ConvexBody Geometry.Plane) : Type

A convex subbody of a fixed solid parent body K: a compact, nonempty, convex Mathlib body whose carrier is contained in K. Elements may be lower-dimensional.

Equations

• NRR.ConvexSubbody K = { C : ConvexBody NRR.Geometry.Plane // ↑C ⊆ K.carrier }

def NRR.ConvexSubbody.body {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : ConvexBody Geometry.Plane

The underlying Mathlib convex body of a subbody.

Equations

• C.body = ↑C

@[instance_reducible]

instance NRR.ConvexSubbody.instCoeHeadSetPlane {K : Geometry.ConvexBody Geometry.Plane} : CoeHead (ConvexSubbody K) (Set Geometry.Plane)

Coercion of a subbody to its underlying carrier set. The ConvexSubbody wrapper is a def over a subtype, so the subtype/root-body coercion chain does not fire automatically; this instance restores (C : Set Plane) through C.body.

Equations

• NRR.ConvexSubbody.instCoeHeadSetPlane = { coe := fun (C : NRR.ConvexSubbody K) => ↑C.body }

theorem NRR.ConvexSubbody.subset_parent {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : ↑C.body ⊆ K.carrier

The carrier of a subbody is contained in the parent body.

noncomputable def NRR.ConvexSubbody.area {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : ℝ

Area of a subbody: the real-valued Lebesgue measure of its carrier.

Equations

• C.area = (MeasureTheory.volume ↑C.body).toReal

@[simp]

theorem NRR.ConvexSubbody.body_carrier {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : ↑C.body = ↑↑C

theorem NRR.ConvexSubbody.convex {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : Convex ℝ ↑C.body

The carrier of a subbody is convex.

theorem NRR.ConvexSubbody.isCompact {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : IsCompact ↑C.body

The carrier of a subbody is compact.

theorem NRR.ConvexSubbody.nonempty {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : (↑C.body).Nonempty

The carrier of a subbody is nonempty.

theorem NRR.ConvexSubbody.area_nonneg {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : 0 ≤ C.area

The area of a subbody is nonnegative.

theorem NRR.ConvexSubbody.area_lt_top {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : MeasureTheory.volume ↑C.body < ⊤

The Lebesgue measure of a subbody is finite (its carrier is compact).

theorem NRR.ConvexSubbody.ext {K : Geometry.ConvexBody Geometry.Plane} {C D : ConvexSubbody K} (h : ↑C.body = ↑D.body) : C = D

Extensionality: two subbodies with equal carriers are equal.

theorem NRR.ConvexSubbody.ext_iff {K : Geometry.ConvexBody Geometry.Plane} {C D : ConvexSubbody K} : C = D ↔ ↑C.body = ↑D.body

def NRR.BodySpace (K : Geometry.ConvexBody Geometry.Plane) (A : ℝ) : Type

The lower-area subspace: subbodies of K whose area is at least A.

Equations

• NRR.BodySpace K A = { C : NRR.ConvexSubbody K // A ≤ C.area }