mathlib3 documentation

linear_algebra.affine_space.finite_dimensional

Finite-dimensional subspaces of affine spaces. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

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) :

The vector_span of a finite set is finite-dimensional.

@[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) :

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

@[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 ι) :

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

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

@[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) :

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

@[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 ι) :

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

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) :

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

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) :

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

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) :

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

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) :

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

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

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) :

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

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) :

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

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) :

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

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) :

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

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) :

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

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) :

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

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) :

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.

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) :

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.

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.

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.

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.

@[protected, instance]

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

@[protected, instance]

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

@[protected, instance]

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

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
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) :

The definition of collinear.

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

Alias of the forward direction of collinear_iff_finrank_le_one.

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.

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) :

The vector_span of collinear points is finite-dimensional.

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) [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] :

The empty set is collinear.

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.

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₀.

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.

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.

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} :

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

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} :

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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₃.

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) :

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

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.

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.

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.

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.

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.

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
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) :

The vector_span of coplanar points is finite-dimensional.

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

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

Alias of the forward direction of coplanar_iff_finrank_le_two.

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.

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) :

Collinear points are coplanar.

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] :

The empty set is coplanar.

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.

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.

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) :

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

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

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} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : collinear k s) (p : P) :

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} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) (h : finite_dimensional.finrank k V = 2) :

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} [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)] :

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} [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.

@[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) :
@[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) :
@[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) :
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) :