# mathlib3documentation

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 #

• collinear defines collinear sets of points as those that span a subspace of dimension at most 1.
theorem finite_dimensional_vector_span_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [ V] [ P] {s : set P} (h : s.finite) :
s)

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} [ 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} [ V] [ P] [finite ι] (p : ι P) (s : set ι) :
(p '' s))

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

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

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} [ 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} [ 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} [ V] [ P] [ V] {p : ι P} (hi : 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} [ V] [ P] [ V] {s : set ι} {f : s P} (hi : 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} [ V] [ P] {p : ι P} (hi : p) {s : finset ι} {n : } (hc : s.card = n + 1) :
s)) = n

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} [ V] [ P] [fintype ι] {p : ι P} (hi : p) {n : } (hc : = n + 1) :
= n

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

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} [ V] [ P] [ V] [fintype ι] {p : ι P} (hi : p) (hc : = ) :

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} [ V] [ P] (p : ι P) (s : finset ι) {n : } (hc : s.card = n + 1) :
s)) n

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} [ V] [ P] [fintype ι] (p : ι P) {n : } (hc : = n + 1) :
n

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} [ V] [ P] [fintype ι] (p : ι P) {n : } (hc : = n + 1) :
= n

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} [ V] [ P] [fintype ι] (p : ι P) {n : } (hc : = n + 1) :
n

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} [ V] [ P] [fintype ι] (p : ι P) {n : } (hc : = 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} [ V] [ P] [fintype ι] (p : ι P) {n : } (hc : = n + 2) :
n

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} [ V] [ P] {p : ι P} (hi : p) {s : finset ι} {sm : V} [ sm] (hle : s) sm) (hc : s.card = ) :
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.

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} [ V] [ P] [fintype ι] {p : ι P} (hi : p) {sm : V} [ sm] (hle : (set.range p) sm) (hc : = ) :
(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.

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} [ V] [ P] {p : ι P} (hi : p) {s : finset ι} {sp : P} [ (sp.direction)] (hle : s) sp) (hc : s.card = ) :
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.

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} [ V] [ P] [fintype ι] {p : ι P} (hi : p) {sp : P} [ (sp.direction)] (hle : (set.range p) sp) (hc : = ) :
(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.

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} [ V] [ P] [ V] [fintype ι] {p : ι P} (hi : p) :

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.

theorem affine.simplex.span_eq_top {k : Type u_1} {V : Type u_2} [ V] [ V] {n : } (T : n) (hrank : = n) :
@[protected, instance]
def finite_dimensional_vector_span_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] (s : P) [ (s.direction)] (p : P) :
s))

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

@[protected, instance]
def finite_dimensional_direction_affine_span_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] (s : P) [ (s.direction)] (p : P) :

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

@[protected, instance]
def finite_dimensional_vector_span_insert_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [ V] [ P] (s : set P) [ s)] (p : P) :
s))

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} [ 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} [ V] [ P] (s : set P) :
s s) 1

The definition of collinear.

theorem collinear_iff_finrank_le_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] {s : set P} [ s)] :
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.

theorem collinear.finrank_le_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] {s : set P} [ s)] :
s 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} [ V] [ P] {s₁ s₂ : set P} (hs : s₁ s₂) (h : s₂) :
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} [ V] [ P] {s : set P} (h : s) :
s)

The vector_span of collinear points is finite-dimensional.

theorem collinear.finite_dimensional_direction_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] {s : set P} (h : 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) [ V] [ P] :

The empty set is collinear.

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

A single point is collinear.

theorem collinear_iff_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] {s : set P} {p₀ : P} (h : p₀ s) :
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} [ V] [ P] (s : set P) :
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} [ V] [ P] (p₁ p₂ : P) :
{p₁, p₂}

Two points are collinear.

theorem affine_independent_iff_not_collinear {k : Type u_1} {V : Type u_2} {P : Type u_3} [ 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} [ 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} [ V] [ P] {p₁ p₂ p₃ : P} :
![p₁, p₂, p₃] ¬ {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} [ V] [ P] {p₁ p₂ p₃ : P} :
{p₁, p₂, p₃} ¬ ![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} [ V] [ P] {p : fin 3 P} {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ i₂) (h₁₃ : i₁ i₃) (h₂₃ : i₂ i₃) :
¬ {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} [ V] [ P] {p : fin 3 P} {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ i₂) (h₁₃ : i₁ i₃) (h₂₃ : i₂ i₃) :
{p i₁, p i₂, p i₃}

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} [ V] [ P] {p₁ p₂ p₃ : P} (h : ¬ {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} [ V] [ P] {p₁ p₂ p₃ : P} (h : ¬ {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} [ V] [ P] {p₁ p₂ p₃ : P} (h : ¬ {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} [ V] [ P] {s : set P} (h : s) {p₁ p₂ p₃ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (hp₃ : p₃ s) (hp₁p₂ : p₁ p₂) :
p₃ {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} [ V] [ P] {s : set P} (h : s) {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) (hp₁p₂ : p₁ p₂) :
{p₁, p₂} = 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} [ V] [ P] {s : set P} (h : s) {p₁ p₂ p₃ : P} (hp₂ : p₂ s) (hp₃ : p₃ s) (hp₂p₃ : p₂ p₃) :
s) {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} [ V] [ P] {s : set P} {p : P} (h : p s) :
s) 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} [ V] [ P] {p₁ p₂ p₃ : P} (h : p₁ {p₂, p₃}) :
{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} [ V] [ P] {p₁ p₂ p₃ p₄ : P} (h₁ : p₁ {p₃, p₄}) (h₂ : p₂ {p₃, p₄}) :
{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} [ V] [ P] {p₁ p₂ p₃ p₄ p₅ : P} (h₁ : p₁ {p₄, p₅}) (h₂ : p₂ {p₄, p₅}) (h₃ : p₃ {p₄, p₅}) :
{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} [ V] [ P] {p₁ p₂ p₃ p₄ p₅ : P} (h₁ : p₁ {p₄, p₅}) (h₂ : p₂ {p₄, p₅}) (h₃ : p₃ {p₄, p₅}) :
{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} [ V] [ P] {p₁ p₂ p₃ p₄ p₅ : P} (h₁ : p₁ {p₄, p₅}) (h₂ : p₂ {p₄, p₅}) (h₃ : p₃ {p₄, p₅}) :
{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} [ 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} [ V] [ P] {s : set P} (h : s) :
s)

The vector_span of coplanar points is finite-dimensional.

theorem coplanar.finite_dimensional_direction_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] {s : set P} (h : 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} [ V] [ P] {s : set P} [ s)] :
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.

theorem coplanar.finrank_le_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] {s : set P} [ s)] :
s 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} [ V] [ P] {s₁ s₂ : set P} (hs : s₁ s₂) (h : s₂) :
s₁

A subset of a coplanar set is coplanar.

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

Collinear points are coplanar.

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

The empty set is coplanar.

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

A single point is coplanar.

theorem coplanar_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [ V] [ P] (p₁ p₂ : P) :
{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} [ V] [ P] {s : set P} {p : P} (h : p s) :
s) s

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

theorem finrank_vector_span_insert_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] (s : P) (p : P) :

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

theorem finrank_vector_span_insert_le_set (k : Type u_1) {V : Type u_2} {P : Type u_3} [ V] [ P] (s : set P) (p : P) :
+ 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} [ V] [ P] {s : set P} (h : s) (p : 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} [ V] [ P] (s : set P) (h : = 2) :
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} [ V] [ P] (s : set P) [h : fact = 2)] :
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} [ V] [ P] (p₁ p₂ p₃ : P) :
{p₁, p₂, p₃}

Three points are coplanar.

@[protected]
theorem affine_basis.finite_dimensional {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [ P] [ V] [finite ι] (b : k P) :
@[protected]
theorem affine_basis.finite {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [ P] [ V] [ V] (b : k P) :
@[protected]
theorem affine_basis.finite_set {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [ P] [ V] [ V] {s : set ι} (b : P) :
theorem affine_basis.card_eq_finrank_add_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [ P] [ V] [fintype ι] (b : k P) :
theorem affine_basis.exists_affine_basis_of_finite_dimensional {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [ P] [ V] [fintype ι] [ V] (h : = ) :