theorem affineSet_iff_eq_mulVec (m n : ℕ) (b : Fin m → ℝ) (B : Matrix (Fin m) (Fin n) ℝ) : IsAffineSet n {x : Fin n → ℝ | B.mulVec x = b} ∧ ∀ (M : Set (Fin n → ℝ)), IsAffineSet n M → ∃ (m' : ℕ) (b' : Fin m' → ℝ) (B' : Matrix (Fin m') (Fin n) ℝ), M = {x : Fin n → ℝ | B'.mulVec x = b'}

Theorem 1.4: Given b ∈ R^m and an m × n real matrix B, the set M = {x ∈ R^n | Bx = b} is an affine set in R^n. Moreover, every affine set in R^n can be represented in this way.

theorem mulVec_eq_sInter_rowSets (m n : ℕ) (B : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) : {x : Fin n → ℝ | B.mulVec x = b} = ⋂₀ ↑(Finset.image (fun (i : Fin m) => {x : Fin n → ℝ | B i ⬝ᵥ x = b i}) Finset.univ)

A matrix fiber is the intersection of its row equation sets.

theorem rowSet_isHyperplane_of_ne_zero (n : ℕ) (b : Fin n → ℝ) (β : ℝ) (hb : b ≠ 0) : IsHyperplane n {x : Fin n → ℝ | x ⬝ᵥ b = β}

A nonzero normal vector gives a hyperplane as a row equation set.

theorem rowSet_eq_univ_or_empty_of_zero (n : ℕ) (β : ℝ) : {x : Fin n → ℝ | 0 ⬝ᵥ x = β} = if β = 0 then Set.univ else ∅

The equation for a zero row is either univ or empty.

theorem empty_eq_sInter_two_hyperplanes (n : ℕ) (hn : 0 < n) : ∃ (S : Finset (Set (Fin n → ℝ))), (∀ H ∈ S, IsHyperplane n H) ∧ ⋂₀ ↑S = ∅

The empty set is a finite intersection of two parallel hyperplanes when n > 0.

theorem affineSet_eq_sInter_hyperplanes (n : ℕ) (M : Set (Fin n → ℝ)) (hn : 0 < n) : IsAffineSet n M → ∃ (S : Finset (Set (Fin n → ℝ))), (∀ H ∈ S, IsHyperplane n H) ∧ M = ⋂₀ ↑S

Corollary 1.4.1. Every affine subset of R^n is an intersection of a finite collection of hyperplanes.

def IsAffinelyIndependent (m n : ℕ) (b : Fin (m + 1) → Fin n → ℝ) : Prop

Text 1.9: A set of m + 1 points b0, b1, ..., bm is said to be affinely independent if aff {b0, b1, ..., bm} is m-dimensional.

Equations

• IsAffinelyIndependent m n b = (affineSetDim n (affineHull n (Set.range b)) ⋯ = ↑m)

theorem isAffinelyIndependent_iff_affineIndependent (m n : ℕ) (b : Fin (m + 1) → Fin n → ℝ) : IsAffinelyIndependent m n b ↔ AffineIndependent ℝ b

Text 1.9 (mathlib): The book's notion agrees with AffineIndependent.

theorem setTranslate_eq_vadd (n : ℕ) (S : Set (Fin n → ℝ)) (a : Fin n → ℝ) : SetTranslate n S a = a +ᵥ S

Translating a set equals pointwise vadd in this commutative setting.

theorem translate_range_sub_eq_union (m n : ℕ) (b0 : Fin n → ℝ) (b : Fin m → Fin n → ℝ) : SetTranslate n ({0} ∪ Set.range fun (i : Fin m) => b i - b0) b0 = {b0} ∪ Set.range b

Translating the difference set by b0 recovers the original points.

theorem affineHull_translate (n : ℕ) (S : Set (Fin n → ℝ)) (a : Fin n → ℝ) : affineHull n (SetTranslate n S a) = SetTranslate n (affineHull n S) a

Affine hull commutes with translation.

theorem affineIndependent_iff_linearIndependent_b0 (m n : ℕ) (b0 : Fin n → ℝ) (b : Fin m → Fin n → ℝ) : (IsAffinelyIndependent m n fun (i : Fin (m + 1)) => Fin.cases (motive := fun (x : Fin (m + 1)) => Fin n → ℝ) b0 (fun (i : Fin m) => b i) i) ↔ LinearIndependent ℝ fun (i : Fin m) => b i - b0

Affine independence of b0, b1, ..., bm is equivalent to linear independence of the difference vectors.

theorem affineHull_eq_translate_and_affineIndependent_iff_linearIndependent (m n : ℕ) (b0 : Fin n → ℝ) (b : Fin m → Fin n → ℝ) : have S := {b0} ∪ Set.range b; have L := affineHull n ({0} ∪ Set.range fun (i : Fin m) => b i - b0); affineHull n S = SetTranslate n L b0 ∧ ((IsAffinelyIndependent m n fun (i : Fin (m + 1)) => Fin.cases (motive := fun (x : Fin (m + 1)) => Fin n → ℝ) b0 (fun (i : Fin m) => b i) i) ↔ LinearIndependent ℝ fun (i : Fin m) => b i - b0)

Text 1.9.1: Let b0, b1, ..., bm ∈ ℝ^n and set L = aff {0, b1 - b0, ..., bm - b0}. Then aff {b0, b1, ..., bm} = b0 + L. Moreover, the points b0, b1, ..., bm are affinely independent if and only if the vectors b1 - b0, ..., bm - b0 are linearly independent.

theorem exists_coeffs_univ_of_mem_affineHull_range {m n : ℕ} {b : Fin (m + 1) → Fin n → ℝ} {x : Fin n → ℝ} (hx : x ∈ affineHull n (Set.range b)) : ∃ (coeffs : Fin (m + 1) → ℝ), ∑ i : Fin (m + 1), coeffs i = 1 ∧ ∑ i : Fin (m + 1), coeffs i • b i = x

Membership in an affine hull of a finite family yields full-index coefficients.

theorem affineIndependent_iff_unique_coeffs_univ (m n : ℕ) (b : Fin (m + 1) → Fin n → ℝ) : AffineIndependent ℝ b ↔ ∀ (coeffs₁ coeffs₂ : Fin (m + 1) → ℝ), ∑ i : Fin (m + 1), coeffs₁ i = 1 → ∑ i : Fin (m + 1), coeffs₂ i = 1 → ∑ i : Fin (m + 1), coeffs₁ i • b i = ∑ i : Fin (m + 1), coeffs₂ i • b i → coeffs₁ = coeffs₂

Affine independence is equivalent to uniqueness of full-index coefficients.

theorem affineHull_exists_affineCombination_and_unique_iff_affineIndependent (m n : ℕ) (b : Fin (m + 1) → Fin n → ℝ) : have M := affineHull n (Set.range b); (∀ x ∈ M, ∃ (coeffs : Fin (m + 1) → ℝ), ∑ i : Fin (m + 1), coeffs i = 1 ∧ ∑ i : Fin (m + 1), coeffs i • b i = x) ∧ (IsAffinelyIndependent m n b ↔ ∀ x ∈ M, ∀ (coeffs₁ coeffs₂ : Fin (m + 1) → ℝ), ∑ i : Fin (m + 1), coeffs₁ i = 1 → ∑ i : Fin (m + 1), coeffs₂ i = 1 → ∑ i : Fin (m + 1), coeffs₁ i • b i = x → ∑ i : Fin (m + 1), coeffs₂ i • b i = x → coeffs₁ = coeffs₂)

Text 1.9.2: Let b0, b1, ..., bm ∈ ℝ^n and set M = aff {b0, b1, ..., bm}. Every point x ∈ M admits a representation x = λ0 b0 + ··· + λm bm with λ0 + ··· + λm = 1. Moreover, the coefficients (λ0, ..., λm) are unique iff the points are affinely independent.