def Set.linealitySpace {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) : Set (EuclideanSpace ℝ (Fin n))

Definition 8.4.2. Let C be a non-empty convex set. The set lin(C) := (-0^+ C) ∩ 0^+ C is called the lineality space of C.

def Set.IsLinearDirection {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (y : EuclideanSpace ℝ (Fin n)) : Prop

Definition 8.4.3. The directions of the vectors y in the lineality space of C are called directions in which C is linear.

def Set.lineality {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) : ℕ

Definition 8.4.4. The dimension of the lineality space lin(C) is called the lineality of C.

theorem linealitySpace_isSubmodule {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCconv : Convex ℝ C) : ∃ (L : Submodule ℝ (EuclideanSpace ℝ (Fin n))), ↑L = C.linealitySpace

The lineality space of a convex set is a submodule.

theorem linealitySpace_subset_direction_affineSpan {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) : C.linealitySpace ⊆ ↑(affineSpan ℝ C).direction

The lineality space is contained in the direction of the affine span.

theorem direction_eq_linealitySpace_of_rank_eq_zero {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hrank : C.rank = 0) : ∃ (L : Submodule ℝ (EuclideanSpace ℝ (Fin n))), ↑L = C.linealitySpace ∧ (affineSpan ℝ C).direction = L

Rank zero forces the affine span direction to be the lineality submodule.

theorem C_eq_translate_linealitySpace {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hrank : C.rank = 0) : ∃ x0 ∈ C, C = (fun (v : EuclideanSpace ℝ (Fin n)) => x0 + v) '' C.linealitySpace

Rank zero implies the set is a translate of its lineality space.

theorem rank_affineSubspace_eq_zero {n : ℕ} (M : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (hM : (↑M).Nonempty) : (↑M).rank = 0

An affine subspace has rank zero.

theorem rank_eq_zero_iff_isAffineSet {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) : C.rank = 0 ↔ IsAffineSet n (⇑(EuclideanSpace.equiv (Fin n) ℝ) '' C)

Theorem 8.4.7. Let C be a non-empty convex set. Then C has rank 0 if and only if C is an affine set.

theorem nonempty_of_isLine {n : ℕ} {L : Set (Fin n → ℝ)} (hL : IsLine n L) : L.Nonempty

A line is nonempty.

theorem rank_eq_dim_iff_lineality_finrank_zero {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCconv : Convex ℝ C) : C.rank = Module.finrank ℝ ↥(affineSpan ℝ C).direction ↔ Module.finrank ℝ ↥(Submodule.span ℝ C.linealitySpace) = 0

Rank equals dimension iff the lineality span has finrank zero.

theorem isLine_of_translate_span_singleton {n : ℕ} {y : Fin n → ℝ} (hy : y ≠ 0) (x0 : Fin n → ℝ) : IsLine n (SetTranslate n (↑(ℝ ∙ y)) x0)

A translate of the span of a nonzero vector is a line.

theorem exists_line_of_nonzero_lineality {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hlin : ∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ 0 ∧ y ∈ C.linealitySpace) : ∃ (L : Set (Fin n → ℝ)), IsLine n L ∧ L ⊆ ⇑(EuclideanSpace.equiv (Fin n) ℝ) '' C

A nonzero lineality direction yields a line contained in the image.

theorem nonzero_lineality_of_line {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCne : C.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hline : ∃ (L : Set (Fin n → ℝ)), IsLine n L ∧ L ⊆ ⇑(EuclideanSpace.equiv (Fin n) ℝ) '' C) : ∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ 0 ∧ y ∈ C.linealitySpace

A line contained in the image yields a nonzero lineality direction.

theorem rank_eq_dim_iff_no_lines {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) : C.rank = Module.finrank ℝ ↥(affineSpan ℝ C).direction ↔ ¬∃ (L : Set (Fin n → ℝ)), IsLine n L ∧ L ⊆ ⇑(EuclideanSpace.equiv (Fin n) ℝ) '' C

Theorem 8.4.8. The rank of a closed convex set equals its dimension if and only if the set contains no lines.