linear_algebra.affine_space.finite_dimensional

source

theorem finite_dimensional_vector_span_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : s.finite) :

finite_dimensional k ↥(vector_span k s)

The vector_span of a finite set is finite-dimensional.

source

@[protected, instance]

def finite_dimensional_vector_span_range (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite ι] (p : ι → P) :

finite_dimensional k ↥(vector_span k (set.range p))

The vector_span of a family indexed by a fintype is finite-dimensional.

source

@[protected, instance]

def finite_dimensional_vector_span_image_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite ι] (p : ι → P) (s : set ι) :

finite_dimensional k ↥(vector_span k (p '' s))

The vector_span of a subset of a family indexed by a fintype is finite-dimensional.

source

theorem finite_dimensional_direction_affine_span_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : s.finite) :

finite_dimensional k ↥((affine_span k s).direction)

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

source

@[protected, instance]

def finite_dimensional_direction_affine_span_range (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite ι] (p : ι → P) :

finite_dimensional k ↥((affine_span k (set.range p)).direction)

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

source

@[protected, instance]

def finite_dimensional_direction_affine_span_image_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite ι] (p : ι → P) (s : set ι) :

finite_dimensional k ↥((affine_span k (p '' s)).direction)

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

source

theorem finite_of_fin_dim_affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite_dimensional k V] {p : ι → P} (hi : affine_independent k p) :

finite ι

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

source

theorem finite_set_of_fin_dim_affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite_dimensional k V] {s : set ι} {f : ↥s → P} (hi : affine_independent k f) :

s.finite

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

source

theorem affine_independent.finrank_vector_span_image_finset {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : ι → P} (hi : affine_independent k p) {s : finset ι} {n : ℕ} (hc : s.card = n + 1) :

finite_dimensional.finrank k ↥(vector_span k ↑(finset.image p s)) = n

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

source

theorem affine_independent.finrank_vector_span {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] {p : ι → P} (hi : affine_independent k p) {n : ℕ} (hc : fintype.card ι = n + 1) :

finite_dimensional.finrank k ↥(vector_span k (set.range p)) = n

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

source

theorem affine_independent.vector_span_eq_top_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite_dimensional k V] [fintype ι] {p : ι → P} (hi : affine_independent k p) (hc : fintype.card ι = finite_dimensional.finrank k V + 1) :

vector_span k (set.range p) = ⊤

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

source

theorem finrank_vector_span_image_finset_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : ι → P) (s : finset ι) {n : ℕ} (hc : s.card = n + 1) :

finite_dimensional.finrank k ↥(vector_span k ↑(finset.image p s)) ≤ n

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

source

theorem finrank_vector_span_range_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 1) :

finite_dimensional.finrank k ↥(vector_span k (set.range p)) ≤ n

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

source

theorem affine_independent_iff_finrank_vector_span_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 1) :

affine_independent k p ↔ finite_dimensional.finrank k ↥(vector_span k (set.range p)) = n

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

source

theorem affine_independent_iff_le_finrank_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 1) :

affine_independent k p ↔ n ≤ finite_dimensional.finrank k ↥(vector_span k (set.range p))

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

source

theorem affine_independent_iff_not_finrank_vector_span_le (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 2) :

affine_independent k p ↔ ¬finite_dimensional.finrank k ↥(vector_span k (set.range p)) ≤ n

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

source

theorem finrank_vector_span_le_iff_not_affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] (p : ι → P) {n : ℕ} (hc : fintype.card ι = n + 2) :

finite_dimensional.finrank k ↥(vector_span k (set.range p)) ≤ n ↔ ¬affine_independent k p

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

source

theorem affine_independent.vector_span_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} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sm : submodule k V} [finite_dimensional k ↥sm] (hle : vector_span k ↑(finset.image p s) ≤ sm) (hc : s.card = finite_dimensional.finrank k ↥sm + 1) :

vector_span k ↑(finset.image p s) = sm

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

source

theorem affine_independent.vector_span_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] {p : ι → P} (hi : affine_independent k p) {sm : submodule k V} [finite_dimensional k ↥sm] (hle : vector_span k (set.range p) ≤ sm) (hc : fintype.card ι = finite_dimensional.finrank k ↥sm + 1) :

vector_span k (set.range p) = sm

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

source

theorem affine_independent.affine_span_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} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sp : affine_subspace k P} [finite_dimensional k ↥(sp.direction)] (hle : affine_span k ↑(finset.image p s) ≤ sp) (hc : s.card = finite_dimensional.finrank k ↥(sp.direction) + 1) :

affine_span k ↑(finset.image p s) = sp

If the affine_span 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.

source

theorem affine_independent.affine_span_eq_of_le_of_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [fintype ι] {p : ι → P} (hi : affine_independent k p) {sp : affine_subspace k P} [finite_dimensional k ↥(sp.direction)] (hle : affine_span k (set.range p) ≤ sp) (hc : fintype.card ι = finite_dimensional.finrank k ↥(sp.direction) + 1) :

affine_span k (set.range p) = sp

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

source

theorem affine_independent.affine_span_eq_top_iff_card_eq_finrank_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [finite_dimensional k V] [fintype ι] {p : ι → P} (hi : affine_independent k p) :

affine_span k (set.range p) = ⊤ ↔ fintype.card ι = finite_dimensional.finrank k V + 1

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

source

theorem affine.simplex.span_eq_top {k : Type u_1} {V : Type u_2} [division_ring k] [add_comm_group V] [module k V] [finite_dimensional k V] {n : ℕ} (T : affine.simplex k V n) (hrank : finite_dimensional.finrank k V = n) :

affine_span k (set.range T.points) = ⊤

source

@[protected, instance]

def finite_dimensional_vector_span_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [finite_dimensional k ↥(s.direction)] (p : P) :

finite_dimensional k ↥(vector_span k (has_insert.insert p ↑s))

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

source

@[protected, instance]

def finite_dimensional_direction_affine_span_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) [finite_dimensional k ↥(s.direction)] (p : P) :

finite_dimensional k ↥((affine_span k (has_insert.insert p ↑s)).direction)

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

source

@[protected, instance]

def finite_dimensional_vector_span_insert_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) [finite_dimensional k ↥(vector_span k s)] (p : P) :

finite_dimensional k ↥(vector_span k (has_insert.insert p s))

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

source

def collinear (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :

Prop

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

Equations

collinear k s = (module.rank k ↥(vector_span k s) ≤ 1)

source

theorem collinear_iff_rank_le_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :

collinear k s ↔ module.rank k ↥(vector_span k s) ≤ 1

The definition of collinear.

source

theorem collinear_iff_finrank_le_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} [finite_dimensional k ↥(vector_span k s)] :

collinear k s ↔ finite_dimensional.finrank k ↥(vector_span k s) ≤ 1

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

source

theorem collinear.finrank_le_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} [finite_dimensional k ↥(vector_span k s)] :

collinear k s → finite_dimensional.finrank k ↥(vector_span k s) ≤ 1

Alias of the forward direction of collinear_iff_finrank_le_one.

source

theorem collinear.subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : set P} (hs : s₁ ⊆ s₂) (h : collinear k s₂) :

collinear k s₁

A subset of a collinear set is collinear.

source

theorem collinear.finite_dimensional_vector_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : collinear k s) :

finite_dimensional k ↥(vector_span k s)

The vector_span of collinear points is finite-dimensional.

source

theorem collinear.finite_dimensional_direction_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : collinear k s) :

finite_dimensional k ↥((affine_span k s).direction)

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

source

theorem collinear_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] :

collinear k ∅

The empty set is collinear.

source

theorem collinear_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) :

collinear k {p}

A single point is collinear.

source

theorem collinear_iff_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p₀ : P} (h : p₀ ∈ s) :

collinear k s ↔ ∃ (v : V), ∀ (p : P), 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₀.

source

theorem collinear_iff_exists_forall_eq_smul_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :

collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ (p : P), 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.

source

theorem collinear_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :

collinear k {p₁, p₂}

Two points are collinear.

source

theorem affine_independent_iff_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : fin 3 → P} :

affine_independent k p ↔ ¬collinear k (set.range p)

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

source

theorem collinear_iff_not_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : fin 3 → P} :

collinear k (set.range p) ↔ ¬affine_independent k p

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

source

theorem affine_independent_iff_not_collinear_set {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ : P} :

affine_independent k ![p₁, p₂, p₃] ↔ ¬collinear k {p₁, p₂, p₃}

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

source

theorem collinear_iff_not_affine_independent_set {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ : P} :

collinear k {p₁, p₂, p₃} ↔ ¬affine_independent k ![p₁, p₂, p₃]

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

source

theorem affine_independent_iff_not_collinear_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : fin 3 → P} {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :

affine_independent k p ↔ ¬collinear k {p i₁, p i₂, p i₃}

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

source

theorem collinear_iff_not_affine_independent_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p : fin 3 → P} {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :

collinear k {p i₁, p i₂, p i₃} ↔ ¬affine_independent k p

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

source

theorem ne₁₂_of_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V 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.

source

theorem ne₁₃_of_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V 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.

source

theorem ne₂₃_of_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V 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.

source

theorem collinear.mem_affine_span_of_mem_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : collinear k s) {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) :

p₃ ∈ affine_span k {p₁, p₂}

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

source

theorem collinear.affine_span_eq_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : collinear k s) {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₁p₂ : p₁ ≠ p₂) :

affine_span k {p₁, p₂} = affine_span k s

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

source

theorem collinear.collinear_insert_iff_of_ne {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : collinear k s) {p₁ p₂ p₃ : P} (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₃ : p₂ ≠ p₃) :

collinear k (has_insert.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₃.

source

theorem collinear_insert_iff_of_mem_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p : P} (h : p ∈ affine_span k s) :

collinear k (has_insert.insert p s) ↔ collinear k s

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

source

theorem collinear_insert_of_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ : P} (h : p₁ ∈ affine_span k {p₂, p₃}) :

collinear k {p₁, p₂, p₃}

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

source

theorem collinear_insert_insert_of_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ p₄ : P} (h₁ : p₁ ∈ affine_span k {p₃, p₄}) (h₂ : p₂ ∈ affine_span 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.

source

theorem collinear_insert_insert_insert_of_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ p₄ p₅ : P} (h₁ : p₁ ∈ affine_span k {p₄, p₅}) (h₂ : p₂ ∈ affine_span k {p₄, p₅}) (h₃ : p₃ ∈ affine_span 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.

source

theorem collinear_insert_insert_insert_left_of_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ p₄ p₅ : P} (h₁ : p₁ ∈ affine_span k {p₄, p₅}) (h₂ : p₂ ∈ affine_span k {p₄, p₅}) (h₃ : p₃ ∈ affine_span 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.

source

theorem collinear_triple_of_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ p₃ p₄ p₅ : P} (h₁ : p₁ ∈ affine_span k {p₄, p₅}) (h₂ : p₂ ∈ affine_span k {p₄, p₅}) (h₃ : p₃ ∈ affine_span 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.

source

def coplanar (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :

Prop

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

Equations

coplanar k s = (module.rank k ↥(vector_span k s) ≤ 2)

source

theorem coplanar.finite_dimensional_vector_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : coplanar k s) :

finite_dimensional k ↥(vector_span k s)

The vector_span of coplanar points is finite-dimensional.

source

theorem coplanar.finite_dimensional_direction_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : coplanar k s) :

finite_dimensional k ↥((affine_span k s).direction)

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

source

theorem coplanar_iff_finrank_le_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} [finite_dimensional k ↥(vector_span k s)] :

coplanar k s ↔ finite_dimensional.finrank k ↥(vector_span k s) ≤ 2

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

source

theorem coplanar.finrank_le_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} [finite_dimensional k ↥(vector_span k s)] :

coplanar k s → finite_dimensional.finrank k ↥(vector_span k s) ≤ 2

Alias of the forward direction of coplanar_iff_finrank_le_two.

source

theorem coplanar.subset {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s₁ s₂ : set P} (hs : s₁ ⊆ s₂) (h : coplanar k s₂) :

coplanar k s₁

A subset of a coplanar set is coplanar.

source

theorem collinear.coplanar {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : collinear k s) :

coplanar k s

Collinear points are coplanar.

source

theorem coplanar_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] :

coplanar k ∅

The empty set is coplanar.

source

theorem coplanar_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) :

coplanar k {p}

A single point is coplanar.

source

theorem coplanar_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ : P) :

coplanar k {p₁, p₂}

Two points are coplanar.

source

theorem coplanar_insert_iff_of_mem_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p : P} (h : p ∈ affine_span k s) :

coplanar k (has_insert.insert p s) ↔ coplanar k s

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

source

theorem finrank_vector_span_insert_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : affine_subspace k P) (p : P) :

finite_dimensional.finrank k ↥(vector_span k (has_insert.insert p ↑s)) ≤ finite_dimensional.finrank k ↥(s.direction) + 1

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

source

theorem finrank_vector_span_insert_le_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) (p : P) :

finite_dimensional.finrank k ↥(vector_span k (has_insert.insert p s)) ≤ finite_dimensional.finrank k ↥(vector_span k s) + 1

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

source

theorem collinear.coplanar_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : collinear k s) (p : P) :

coplanar k (has_insert.insert p s)

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

source

theorem coplanar_of_finrank_eq_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) (h : finite_dimensional.finrank k V = 2) :

coplanar k s

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

source

theorem coplanar_of_fact_finrank_eq_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) [h : fact (finite_dimensional.finrank k V = 2)] :

coplanar k s

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

source

theorem coplanar_triple (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (p₁ p₂ p₃ : P) :

coplanar k {p₁, p₂, p₃}

Three points are coplanar.

source

@[protected]

theorem affine_basis.finite_dimensional {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] [finite ι] (b : affine_basis ι k P) :

finite_dimensional k V

source

@[protected]

theorem affine_basis.finite {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] [finite_dimensional k V] (b : affine_basis ι k P) :

finite ι

source

@[protected]

theorem affine_basis.finite_set {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] [finite_dimensional k V] {s : set ι} (b : affine_basis ↥s k P) :

s.finite

source

theorem affine_basis.card_eq_finrank_add_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] [fintype ι] (b : affine_basis ι k P) :

fintype.card ι = finite_dimensional.finrank k V + 1

source

theorem affine_basis.exists_affine_basis_of_finite_dimensional {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [add_comm_group V] [add_torsor V P] [division_ring k] [module k V] [fintype ι] [finite_dimensional k V] (h : fintype.card ι = finite_dimensional.finrank k V + 1) :

nonempty (affine_basis ι k P)

mathlib3 documentation

Finite-dimensional subspaces of affine spaces. #

Main definitions #