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 ↥(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 ↥(vectorSpan k (Set.range p))

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

Equations

• (_ : FiniteDimensional k ↥(vectorSpan k (Set.range p))) = (_ : FiniteDimensional k ↥(vectorSpan k (Set.range p)))

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 ↥(vectorSpan k (p '' s))

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

Equations

• (_ : FiniteDimensional k ↥(vectorSpan k (p '' s))) = (_ : FiniteDimensional k ↥(vectorSpan k (p '' s)))

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 ↥(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 ↥(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 k ↥(AffineSubspace.direction (affineSpan k (Set.range p)))) = (_ : FiniteDimensional k ↥(AffineSubspace.direction (affineSpan k (Set.range p))))

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 ↥(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 k ↥(AffineSubspace.direction (affineSpan k (p '' s)))) = (_ : FiniteDimensional k ↥(AffineSubspace.direction (affineSpan k (p '' s))))

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 : s.card = n + 1) : FiniteDimensional.finrank k ↥(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 ↥(vectorSpan k (Set.range p)) = n

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

theorem AffineIndependent.finrank_vectorSpan_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 ι] [Nonempty ι] {p : ι → P} (hi : AffineIndependent k p) : FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι

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 : s.card = n + 1) : FiniteDimensional.finrank k ↥(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 ↥(vectorSpan k (Set.range p)) ≤ n

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

theorem finrank_vectorSpan_range_add_one_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 ι] [Nonempty ι] (p : ι → P) : FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1 ≤ Fintype.card ι

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 ↥(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 ↥(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 ↥(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 ↥(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.card_le_finrank_succ {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} (hp : AffineIndependent k p) : Fintype.card ι ≤ FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1

theorem AffineIndependent.card_le_card_of_subset_affineSpan {k : Type u_1} {V : Type u_2} [DivisionRing k] [AddCommGroup V] [Module k V] {s : Finset V} {t : Finset V} (hs : AffineIndependent k Subtype.val) (hst : ↑s ⊆ ↑(affineSpan k ↑t)) : s.card ≤ t.card

If an affine independent finset is contained in the affine span of another finset, then its cardinality is at most the cardinality of that finset.

theorem AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan {k : Type u_1} {V : Type u_2} [DivisionRing k] [AddCommGroup V] [Module k V] {s : Finset V} {t : Finset V} (hs : AffineIndependent k Subtype.val) (hst : affineSpan k ↑s < affineSpan k ↑t) : s.card < t.card

If the affine span of an affine independent finset is strictly contained in the affine span of another finset, then its cardinality is strictly less than the cardinality of that finset.

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 ↥sm] (hle : vectorSpan k ↑(Finset.image p s) ≤ sm) (hc : s.card = FiniteDimensional.finrank k ↥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 ↥sm] (hle : vectorSpan k (Set.range p) ≤ sm) (hc : Fintype.card ι = FiniteDimensional.finrank k ↥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 ↥(AffineSubspace.direction sp)] (hle : affineSpan k ↑(Finset.image p s) ≤ sp) (hc : s.card = FiniteDimensional.finrank k ↥(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 ↥(AffineSubspace.direction sp)] (hle : affineSpan k (Set.range p) ≤ sp) (hc : Fintype.card ι = FiniteDimensional.finrank k ↥(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 ↥(AffineSubspace.direction s)] (p : P) : FiniteDimensional k ↥(vectorSpan k (insert p ↑s))

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

Equations

• (_ : FiniteDimensional k ↥(vectorSpan k (insert p ↑s))) = (_ : FiniteDimensional k ↥(vectorSpan k (insert p ↑s)))

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 ↥(AffineSubspace.direction s)] (p : P) : FiniteDimensional k ↥(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 k ↥(AffineSubspace.direction (affineSpan k (insert p ↑s)))) = (_ : FiniteDimensional k ↥(AffineSubspace.direction (affineSpan k (insert p ↑s))))

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 ↥(vectorSpan k s)] (p : P) : FiniteDimensional k ↥(vectorSpan k (insert p s))

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

Equations

• (_ : FiniteDimensional k ↥(vectorSpan k (insert p s))) = (_ : FiniteDimensional k ↥(vectorSpan k (insert p s)))

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 ↥(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 ↥(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 ↥(vectorSpan k s)] : Collinear k s ↔ FiniteDimensional.finrank k ↥(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 ↥(vectorSpan k s)] : Collinear k s → FiniteDimensional.finrank k ↥(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 ↥(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 ↥(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 : V), ∀ p ∈ s, ∃ (r : k), 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₀ : P) (v : V), ∀ p ∈ s, ∃ (r : k), 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 ↥(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 ↥(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 ↥(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 ↥(vectorSpan k s)] : Coplanar k s ↔ FiniteDimensional.finrank k ↥(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 ↥(vectorSpan k s)] : Coplanar k s → FiniteDimensional.finrank k ↥(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 ↥(vectorSpan k (insert p ↑s)) ≤ FiniteDimensional.finrank k ↥(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 ↥(vectorSpan k (insert p s)) ≤ FiniteDimensional.finrank k ↥(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)