Finite-dimensional subspaces of affine spaces.

This file provides a few results relating to finite-dimensional subspaces of affine spaces.

Main definitions

• Collinear defines collinear sets of points as those that span a subspace of dimension at most 1.

theorem finiteDimensional_vectorSpan_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Set.Finite s) : FiniteDimensional k { x // x ∈ vectorSpan k s }

The vectorSpan of a finite set is finite-dimensional.

instance finiteDimensional_vectorSpan_range (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Finite ι] (p : ι → P) : FiniteDimensional k { x // x ∈ vectorSpan k (Set.range p) }

The vectorSpan of a family indexed by a Fintype is finite-dimensional.

Equations

• finiteDimensional_vectorSpan_range = finiteDimensional_vectorSpan_range.proof_1

instance finiteDimensional_vectorSpan_image_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Finite ι] (p : ι → P) (s : Set ι) : FiniteDimensional k { x // x ∈ vectorSpan k (p '' s) }

The vectorSpan of a subset of a family indexed by a Fintype is finite-dimensional.

Equations

• finiteDimensional_vectorSpan_image_of_finite = finiteDimensional_vectorSpan_image_of_finite.proof_1

theorem finiteDimensional_direction_affineSpan_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Set.Finite s) : FiniteDimensional k { x // x ∈ AffineSubspace.direction (affineSpan k s) }

The direction of the affine span of a finite set is finite-dimensional.

instance finiteDimensional_direction_affineSpan_range (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Finite ι] (p : ι → P) : FiniteDimensional k { x // x ∈ AffineSubspace.direction (affineSpan k (Set.range p)) }

The direction of the affine span of a family indexed by a Fintype is finite-dimensional.

Equations

• finiteDimensional_direction_affineSpan_range = finiteDimensional_direction_affineSpan_range.proof_1

instance finiteDimensional_direction_affineSpan_image_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Finite ι] (p : ι → P) (s : Set ι) : FiniteDimensional k { x // x ∈ AffineSubspace.direction (affineSpan k (p '' s)) }

The direction of the affine span of a subset of a family indexed by a Fintype is finite-dimensional.

Equations

• finiteDimensional_direction_affineSpan_image_of_finite = finiteDimensional_direction_affineSpan_image_of_finite.proof_1

theorem finite_of_fin_dim_affineIndependent (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [FiniteDimensional k V] {p : ι → P} (hi : AffineIndependent k p) : Finite ι

An affine-independent family of points in a finite-dimensional affine space is finite.

theorem finite_set_of_fin_dim_affineIndependent (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [FiniteDimensional k V] {s : Set ι} {f : ↑s → P} (hi : AffineIndependent k f) : Set.Finite s

An affine-independent subset of a finite-dimensional affine space is finite.

theorem AffineIndependent.finrank_vectorSpan_image_finset {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [DecidableEq P] {p : ι → P} (hi : AffineIndependent k p) {s : Finset ι} {n : ℕ} (hc : Finset.card s = n + 1) : FiniteDimensional.finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } = n

The vectorSpan of a finite subset of an affinely independent family has dimension one less than its cardinality.

theorem AffineIndependent.finrank_vectorSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] {p : ι → P} (hi : AffineIndependent k p) {n : ℕ} (hc : Fintype.card ι = n + 1) : FiniteDimensional.finrank k { x // x ∈ vectorSpan k (Set.range p) } = n

The vectorSpan of a finite affinely independent family has dimension one less than its cardinality.

theorem AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [FiniteDimensional k V] [Fintype ι] {p : ι → P} (hi : AffineIndependent k p) (hc : Fintype.card ι = FiniteDimensional.finrank k V + 1) : vectorSpan k (Set.range p) = ⊤

The vectorSpan of a finite affinely independent family whose cardinality is one more than that of the finite-dimensional space is ⊤.

theorem finrank_vectorSpan_image_finset_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [DecidableEq P] (p : ι → P) (s : Finset ι) {n : ℕ} (hc : Finset.card s = n + 1) : FiniteDimensional.finrank k { x // x ∈ vectorSpan k ↑(Finset.image p s) } ≤ n

The vectorSpan of n + 1 points in an indexed family has dimension at most n.

theorem finrank_vectorSpan_range_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 1) : FiniteDimensional.finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ n

The vectorSpan of an indexed family of n + 1 points has dimension at most n.

theorem affineIndependent_iff_finrank_vectorSpan_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 1) : AffineIndependent k p ↔ FiniteDimensional.finrank k { x // x ∈ vectorSpan k (Set.range p) } = n

n + 1 points are affinely independent if and only if their vectorSpan has dimension n.

theorem affineIndependent_iff_le_finrank_vectorSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 1) : AffineIndependent k p ↔ n ≤ FiniteDimensional.finrank k { x // x ∈ vectorSpan k (Set.range p) }

n + 1 points are affinely independent if and only if their vectorSpan has dimension at least n.

theorem affineIndependent_iff_not_finrank_vectorSpan_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 2) : AffineIndependent k p ↔ ¬FiniteDimensional.finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ n

n + 2 points are affinely independent if and only if their vectorSpan does not have dimension at most n.

theorem finrank_vectorSpan_le_iff_not_affineIndependent (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 2) : FiniteDimensional.finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ n ↔ ¬AffineIndependent k p

n + 2 points have a vectorSpan with dimension at most n if and only if they are not affinely independent.

theorem AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [DecidableEq P] {p : ι → P} (hi : AffineIndependent k p) {s : Finset ι} {sm : Submodule k V} [FiniteDimensional k { x // x ∈ sm }] (hle : vectorSpan k ↑(Finset.image p s) ≤ sm) (hc : Finset.card s = FiniteDimensional.finrank k { x // x ∈ sm } + 1) : vectorSpan k ↑(Finset.image p s) = sm

If the vectorSpan of a finite subset of an affinely independent family lies in a submodule with dimension one less than its cardinality, it equals that submodule.

theorem AffineIndependent.vectorSpan_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] {p : ι → P} (hi : AffineIndependent k p) {sm : Submodule k V} [FiniteDimensional k { x // x ∈ sm }] (hle : vectorSpan k (Set.range p) ≤ sm) (hc : Fintype.card ι = FiniteDimensional.finrank k { x // x ∈ sm } + 1) : vectorSpan k (Set.range p) = sm

If the vectorSpan of a finite affinely independent family lies in a submodule with dimension one less than its cardinality, it equals that submodule.

theorem AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [DecidableEq P] {p : ι → P} (hi : AffineIndependent k p) {s : Finset ι} {sp : AffineSubspace k P} [FiniteDimensional k { x // x ∈ AffineSubspace.direction sp }] (hle : affineSpan k ↑(Finset.image p s) ≤ sp) (hc : Finset.card s = FiniteDimensional.finrank k { x // x ∈ AffineSubspace.direction sp } + 1) : affineSpan k ↑(Finset.image p s) = sp

If the affineSpan of a finite subset of an affinely independent family lies in an affine subspace whose direction has dimension one less than its cardinality, it equals that subspace.

theorem AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] {p : ι → P} (hi : AffineIndependent k p) {sp : AffineSubspace k P} [FiniteDimensional k { x // x ∈ AffineSubspace.direction sp }] (hle : affineSpan k (Set.range p) ≤ sp) (hc : Fintype.card ι = FiniteDimensional.finrank k { x // x ∈ AffineSubspace.direction sp } + 1) : affineSpan k (Set.range p) = sp

If the affineSpan of a finite affinely independent family lies in an affine subspace whose direction has dimension one less than its cardinality, it equals that subspace.

theorem AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [FiniteDimensional k V] [Fintype ι] {p : ι → P} (hi : AffineIndependent k p) : affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = FiniteDimensional.finrank k V + 1

The affineSpan of a finite affinely independent family is ⊤ iff the family's cardinality is one more than that of the finite-dimensional space.

theorem Affine.Simplex.span_eq_top {k : Type u_1} {V : Type u_2} [DivisionRing k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {n : ℕ} (T : Affine.Simplex k V n) (hrank : FiniteDimensional.finrank k V = n) : affineSpan k (Set.range T.points) = ⊤

instance finiteDimensional_vectorSpan_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [FiniteDimensional k { x // x ∈ AffineSubspace.direction s }] (p : P) : FiniteDimensional k { x // x ∈ vectorSpan k (insert p ↑s) }

The vectorSpan of adding a point to a finite-dimensional subspace is finite-dimensional.

Equations

• @finiteDimensional_vectorSpan_insert = @finiteDimensional_vectorSpan_insert.proof_1

instance finiteDimensional_direction_affineSpan_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [FiniteDimensional k { x // x ∈ AffineSubspace.direction s }] (p : P) : FiniteDimensional k { x // x ∈ AffineSubspace.direction (affineSpan k (insert p ↑s)) }

The direction of the affine span of adding a point to a finite-dimensional subspace is finite-dimensional.

Equations

• @finiteDimensional_direction_affineSpan_insert = @finiteDimensional_direction_affineSpan_insert.proof_1

instance finiteDimensional_vectorSpan_insert_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) [FiniteDimensional k { x // x ∈ vectorSpan k s }] (p : P) : FiniteDimensional k { x // x ∈ vectorSpan k (insert p s) }

The vectorSpan of adding a point to a set with a finite-dimensional vectorSpan is finite-dimensional.

Equations

• finiteDimensional_vectorSpan_insert_set = finiteDimensional_vectorSpan_insert_set.proof_1

def Collinear (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) : Prop

A set of points is collinear if their vectorSpan has dimension at most 1.

Equations

• Collinear k s = (Module.rank k { x // x ∈ vectorSpan k s } ≤ 1)

theorem collinear_iff_rank_le_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) : Collinear k s ↔ Module.rank k { x // x ∈ vectorSpan k s } ≤ 1

The definition of Collinear.

theorem collinear_iff_finrank_le_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} [FiniteDimensional k { x // x ∈ vectorSpan k s }] : Collinear k s ↔ FiniteDimensional.finrank k { x // x ∈ vectorSpan k s } ≤ 1

A set of points, whose vectorSpan is finite-dimensional, is collinear if and only if their vectorSpan has dimension at most 1.

theorem Collinear.finrank_le_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} [FiniteDimensional k { x // x ∈ vectorSpan k s }] : Collinear k s → FiniteDimensional.finrank k { x // x ∈ vectorSpan k s } ≤ 1

Alias of the forward direction of collinear_iff_finrank_le_one.

---

A set of points, whose vectorSpan is finite-dimensional, is collinear if and only if their vectorSpan has dimension at most 1.

theorem Collinear.subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : Set P} {s₂ : Set P} (hs : s₁ ⊆ s₂) (h : Collinear k s₂) : Collinear k s₁

A subset of a collinear set is collinear.

theorem Collinear.finiteDimensional_vectorSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Collinear k s) : FiniteDimensional k { x // x ∈ vectorSpan k s }

The vectorSpan of collinear points is finite-dimensional.

theorem Collinear.finiteDimensional_direction_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Collinear k s) : FiniteDimensional k { x // x ∈ AffineSubspace.direction (affineSpan k s) }

The direction of the affine span of collinear points is finite-dimensional.

theorem collinear_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] : Collinear k ∅

The empty set is collinear.

theorem collinear_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) : Collinear k {p}

A single point is collinear.

theorem collinear_iff_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p₀ : P} (h : p₀ ∈ s) : Collinear k s ↔ ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀

Given a point p₀ in a set of points, that set is collinear if and only if the points can all be expressed as multiples of the same vector, added to p₀.

theorem collinear_iff_exists_forall_eq_smul_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) : Collinear k s ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀

A set of points is collinear if and only if they can all be expressed as multiples of the same vector, added to the same base point.

theorem collinear_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) : Collinear k {p₁, p₂}

Two points are collinear.

theorem affineIndependent_iff_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : Fin 3 → P} : AffineIndependent k p ↔ ¬Collinear k (Set.range p)

Three points are affinely independent if and only if they are not collinear.

theorem collinear_iff_not_affineIndependent {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : Fin 3 → P} : Collinear k (Set.range p) ↔ ¬AffineIndependent k p

Three points are collinear if and only if they are not affinely independent.

theorem affineIndependent_iff_not_collinear_set {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} : AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k {p₁, p₂, p₃}

Three points are affinely independent if and only if they are not collinear.

theorem collinear_iff_not_affineIndependent_set {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} : Collinear k {p₁, p₂, p₃} ↔ ¬AffineIndependent k ![p₁, p₂, p₃]

Three points are collinear if and only if they are not affinely independent.

theorem affineIndependent_iff_not_collinear_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : Fin 3 → P} {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}

Three points are affinely independent if and only if they are not collinear.

theorem collinear_iff_not_affineIndependent_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : Fin 3 → P} {i₁ : Fin 3} {i₂ : Fin 3} {i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Collinear k {p i₁, p i₂, p i₃} ↔ ¬AffineIndependent k p

Three points are collinear if and only if they are not affinely independent.

theorem ne₁₂_of_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear k {p₁, p₂, p₃}) : p₁ ≠ p₂

If three points are not collinear, the first and second are different.

theorem ne₁₃_of_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear k {p₁, p₂, p₃}) : p₁ ≠ p₃

If three points are not collinear, the first and third are different.

theorem ne₂₃_of_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : ¬Collinear k {p₁, p₂, p₃}) : p₂ ≠ p₃

If three points are not collinear, the second and third are different.

theorem Collinear.mem_affineSpan_of_mem_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Collinear k s) {p₁ : P} {p₂ : P} {p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) : p₃ ∈ affineSpan k {p₁, p₂}

A point in a collinear set of points lies in the affine span of any two distinct points of that set.

theorem Collinear.affineSpan_eq_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Collinear k s) {p₁ : P} {p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₁p₂ : p₁ ≠ p₂) : affineSpan k {p₁, p₂} = affineSpan k s

The affine span of any two distinct points of a collinear set of points equals the affine span of the whole set.

theorem Collinear.collinear_insert_iff_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Collinear k s) {p₁ : P} {p₂ : P} {p₃ : P} (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₃ : p₂ ≠ p₃) : Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}

Given a collinear set of points, and two distinct points p₂ and p₃ in it, a point p₁ is collinear with the set if and only if it is collinear with p₂ and p₃.

theorem collinear_insert_iff_of_mem_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p : P} (h : p ∈ affineSpan k s) : Collinear k (insert p s) ↔ Collinear k s

Adding a point in the affine span of a set does not change whether that set is collinear.

theorem collinear_insert_of_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : p₁ ∈ affineSpan k {p₂, p₃}) : Collinear k {p₁, p₂, p₃}

If a point lies in the affine span of two points, those three points are collinear.

theorem collinear_insert_insert_of_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} (h₁ : p₁ ∈ affineSpan k {p₃, p₄}) (h₂ : p₂ ∈ affineSpan k {p₃, p₄}) : Collinear k {p₁, p₂, p₃, p₄}

If two points lie in the affine span of two points, those four points are collinear.

theorem collinear_insert_insert_insert_of_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} (h₁ : p₁ ∈ affineSpan k {p₄, p₅}) (h₂ : p₂ ∈ affineSpan k {p₄, p₅}) (h₃ : p₃ ∈ affineSpan k {p₄, p₅}) : Collinear k {p₁, p₂, p₃, p₄, p₅}

If three points lie in the affine span of two points, those five points are collinear.

theorem collinear_insert_insert_insert_left_of_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} (h₁ : p₁ ∈ affineSpan k {p₄, p₅}) (h₂ : p₂ ∈ affineSpan k {p₄, p₅}) (h₃ : p₃ ∈ affineSpan k {p₄, p₅}) : Collinear k {p₁, p₂, p₃, p₄}

If three points lie in the affine span of two points, the first four points are collinear.

theorem collinear_triple_of_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} {p₅ : P} (h₁ : p₁ ∈ affineSpan k {p₄, p₅}) (h₂ : p₂ ∈ affineSpan k {p₄, p₅}) (h₃ : p₃ ∈ affineSpan k {p₄, p₅}) : Collinear k {p₁, p₂, p₃}

If three points lie in the affine span of two points, the first three points are collinear.

def Coplanar (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) : Prop

A set of points is coplanar if their vectorSpan has dimension at most 2.

Equations

• Coplanar k s = (Module.rank k { x // x ∈ vectorSpan k s } ≤ 2)

theorem Coplanar.finiteDimensional_vectorSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Coplanar k s) : FiniteDimensional k { x // x ∈ vectorSpan k s }

The vectorSpan of coplanar points is finite-dimensional.

theorem Coplanar.finiteDimensional_direction_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Coplanar k s) : FiniteDimensional k { x // x ∈ AffineSubspace.direction (affineSpan k s) }

The direction of the affine span of coplanar points is finite-dimensional.

theorem coplanar_iff_finrank_le_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} [FiniteDimensional k { x // x ∈ vectorSpan k s }] : Coplanar k s ↔ FiniteDimensional.finrank k { x // x ∈ vectorSpan k s } ≤ 2

A set of points, whose vectorSpan is finite-dimensional, is coplanar if and only if their vectorSpan has dimension at most 2.

theorem Coplanar.finrank_le_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} [FiniteDimensional k { x // x ∈ vectorSpan k s }] : Coplanar k s → FiniteDimensional.finrank k { x // x ∈ vectorSpan k s } ≤ 2

Alias of the forward direction of coplanar_iff_finrank_le_two.

---

A set of points, whose vectorSpan is finite-dimensional, is coplanar if and only if their vectorSpan has dimension at most 2.

theorem Coplanar.subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : Set P} {s₂ : Set P} (hs : s₁ ⊆ s₂) (h : Coplanar k s₂) : Coplanar k s₁

A subset of a coplanar set is coplanar.

theorem Collinear.coplanar {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Collinear k s) : Coplanar k s

Collinear points are coplanar.

theorem coplanar_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] : Coplanar k ∅

The empty set is coplanar.

theorem coplanar_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) : Coplanar k {p}

A single point is coplanar.

theorem coplanar_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) : Coplanar k {p₁, p₂}

Two points are coplanar.

theorem coplanar_insert_iff_of_mem_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p : P} (h : p ∈ affineSpan k s) : Coplanar k (insert p s) ↔ Coplanar k s

Adding a point in the affine span of a set does not change whether that set is coplanar.

theorem finrank_vectorSpan_insert_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) (p : P) : FiniteDimensional.finrank k { x // x ∈ vectorSpan k (insert p ↑s) } ≤ FiniteDimensional.finrank k { x // x ∈ AffineSubspace.direction s } + 1

Adding a point to a finite-dimensional subspace increases the dimension by at most one.

theorem finrank_vectorSpan_insert_le_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) (p : P) : FiniteDimensional.finrank k { x // x ∈ vectorSpan k (insert p s) } ≤ FiniteDimensional.finrank k { x // x ∈ vectorSpan k s } + 1

Adding a point to a set with a finite-dimensional span increases the dimension by at most one.

theorem Collinear.coplanar_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : Collinear k s) (p : P) : Coplanar k (insert p s)

Adding a point to a collinear set produces a coplanar set.

theorem coplanar_of_finrank_eq_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) (h : FiniteDimensional.finrank k V = 2) : Coplanar k s

A set of points in a two-dimensional space is coplanar.

theorem coplanar_of_fact_finrank_eq_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) [h : Fact (FiniteDimensional.finrank k V = 2)] : Coplanar k s

A set of points in a two-dimensional space is coplanar.

theorem coplanar_triple (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) (p₃ : P) : Coplanar k {p₁, p₂, p₃}

Three points are coplanar.

theorem AffineBasis.finiteDimensional {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] [Finite ι] (b : AffineBasis ι k P) : FiniteDimensional k V

theorem AffineBasis.finite {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] [FiniteDimensional k V] (b : AffineBasis ι k P) : Finite ι

theorem AffineBasis.finite_set {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] [FiniteDimensional k V] {s : Set ι} (b : AffineBasis (↑s) k P) : Set.Finite s

theorem AffineBasis.card_eq_finrank_add_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] [Fintype ι] (b : AffineBasis ι k P) : Fintype.card ι = FiniteDimensional.finrank k V + 1

theorem AffineBasis.exists_affineBasis_of_finiteDimensional {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] [Fintype ι] [FiniteDimensional k V] (h : Fintype.card ι = FiniteDimensional.finrank k V + 1) : Nonempty (AffineBasis ι k P)