structure AffineHyperplane (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Type u_1

An affine hyperplane $H = \{x ∈ E : ⟨n, x⟩ = c\}$ specified by a nonzero normal vector $n$ and an offset $c$.

• normal : E
• offset : ℝ
• normal_ne_zero : self.normal ≠ 0

def AffineHyperplane.carrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) : Set E

The underlying set $\{x : ⟨n, x⟩ = c\}$ of the affine hyperplane.

def AffineHyperplane.positiveHalfSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) : Set E

The open positive half-space $\{x : ⟨n, x⟩ > c\}$.

def AffineHyperplane.negativeHalfSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) : Set E

The open negative half-space $\{x : ⟨n, x⟩ < c\}$.

def AffineHyperplane.Separates {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) (x y : E) : Prop

The hyperplane $h$ separates $x$ and $y$ if they lie in opposite open half-spaces.

def AffineHyperplane.IsWall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η : AffineHyperplane E) (C : Set E) : Prop

$η$ is a wall of $C$ if some open neighborhood of a point of $η$ meets $η$ inside the closure of $C$.

noncomputable def AffineHyperplane.basePoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) : E

A canonical base point of $η$: the orthogonal projection of $0$ onto $η$.

noncomputable def AffineHyperplane.direction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) : Submodule ℝ E

The direction subspace (parallel translate to the origin) of $η$, equal to $n^⊥$.

theorem AffineHyperplane.basePoint_mem_carrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) : h.basePoint ∈ h.carrier

The base point lies on the hyperplane.

def AffineHyperplane.toAffineSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (h : AffineHyperplane E) : AffineSubspace ℝ E

The affine hyperplane viewed as a Mathlib AffineSubspace.

instance AffineHyperplane.instNonemptyToAffineSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (h : AffineHyperplane E) : Nonempty ↥h.toAffineSubspace

The affine subspace associated to a hyperplane is nonempty (it contains the base point).

noncomputable def AffineHyperplane.reflectionMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (h : AffineHyperplane E) : E ≃ᵃⁱ[ℝ] E

The Euclidean reflection $E ≃ᵃⁱ E$ across the affine hyperplane $η$.

structure HyperplaneArrangement (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Type u_2

A hyperplane arrangement on $E$: simply a set of affine hyperplanes.

• hyperplanes : Set (AffineHyperplane E)

def HyperplaneArrangement.unionSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) : Set E

The union $\bigcup_{η ∈ \mathcal A} η$ of all hyperplanes in the arrangement.

def HyperplaneArrangement.complement {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) : Set E

The complement of the arrangement: points lying on no hyperplane.

def HyperplaneArrangement.IsLocallyFinite {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) : Prop

An arrangement is locally finite if around every point only finitely many hyperplanes meet a small open ball.

structure HyperplaneArrangement.Chamber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) : Type u_1

A chamber of an arrangement: a maximal connected subset of the complement of all hyperplanes.

• set : Set E
• subset_complement : self.set ⊆ arr.complement
• isConnected : IsConnected self.set
• is_maximal (S : Set E) : S ⊆ arr.complement → IsConnected S → self.set ⊆ S → S ⊆ self.set

def HyperplaneArrangement.SeparatedBy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (x y : E) : Prop

Two points are separated by the arrangement if some hyperplane separates them.

theorem HalfSpaceConvex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) : Convex ℝ h.positiveHalfSpace

Open half-spaces are convex.

theorem HalfSpaceOpen {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : AffineHyperplane E) : IsOpen h.positiveHalfSpace

Open half-spaces are open subsets of $E$.