NRR.HalfSpace — public halfspace definitions

Provides the set-theoretic lower and upper halfspaces used throughout the cut and power-diagram layers. Measure-theoretic and continuity results live in the dedicated halfspace-cut modules.

def NRR.Halfspace.of (u : E2) (c : ℝ) : Set E2

The public closed half‑space with inner normal u and offset c, defined as a direct wrapper around the implemented geometry half‑space Geometry.lowerClosedHalfspace u c, i.e. {x : E2 | ⟪u, x⟫ ≤ c}. (E2 is a definitional alias of Geometry.Plane.)

Equations

• NRR.Halfspace.of u c = NRR.Geometry.lowerClosedHalfspace u c

@[simp]

theorem NRR.Halfspace.of_eq_lowerClosedHalfspace (u : E2) (c : ℝ) : of u c = Geometry.lowerClosedHalfspace u c

theorem NRR.Halfspace.convex (u : E2) (c : ℝ) : Convex ℝ (of u c)

A half‑space is convex.

theorem NRR.Halfspace.isClosed (u : E2) (c : ℝ) : IsClosed (of u c)

A half‑space is closed.

theorem NRR.Halfspace.mem_halfspace (u x : E2) (c : ℝ) : x ∈ of u c ↔ inner ℝ u x ≤ c

theorem NRR.Halfspace.hyperplane_null {u : E2} (hu : u ≠ 0) (c : ℝ) : MeasureTheory.volume {x : E2 | inner ℝ u x = c} = 0

An affine hyperplane {x | ⟪u, x⟫ = c} in the plane, with nonzero normal u, has Lebesgue measure zero. The hyperplane is a translate of the kernel of the (nonzero) linear functional ⟪u, ·⟫, which is a proper submodule and hence Haar-null.

noncomputable def NRR.Geometry.ConvexBody.interHalfspace (K : ConvexBody Plane) (u : Plane) (c : ℝ) (hInt : (interior (K.carrier ∩ Halfspace.of u c)).Nonempty) : ConvexBody Plane

Intersecting a convex body K with the public closed half‑space Halfspace.of u c yields a compact convex set; when it retains nonempty interior it is again a (solid) convex body. This bundles the intersection as a ConvexBody, requiring the nonempty‑interior hypothesis hInt explicitly (solidity is not automatic). It is a thin wrapper around the geometry primitive ConvexBody.cutLowerClosed.

Equations

• K.interHalfspace u c hInt = K.cutLowerClosed u c hInt

@[simp]

theorem NRR.Geometry.ConvexBody.coe_interHalfspace (K : ConvexBody Plane) (u : Plane) (c : ℝ) (hInt : (interior (K.carrier ∩ Halfspace.of u c)).Nonempty) : (K.interHalfspace u c hInt).carrier = K.carrier ∩ Halfspace.of u c

The carrier of interHalfspace is the set intersection with the public half‑space.