# mathlibdocumentation

linear_algebra.affine_space.finite_dimensional

# 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 finite_dimensional_vector_span_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {s : set P} (h : s.finite) :
s)

The vector_span of a finite set is finite-dimensional.

@[instance]
def finite_dimensional_vector_span_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [fintype ι] (p : ι → P) :

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

@[instance]
def finite_dimensional_vector_span_image_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [fintype ι] (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} [field k] [ V] [ P] {s : set P} (h : s.finite) :

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

@[instance]
def finite_dimensional_direction_affine_span_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [fintype ι] (p : ι → P) :

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

@[instance]
def finite_dimensional_direction_affine_span_image_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [fintype ι] (p : ι → P) (s : set ι) :

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

theorem findim_vector_span_image_finset_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} {p : ι → P} (hi : p) {s : finset ι} {n : } (hc : s.card = n + 1) :
(p '' s)) = n

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

theorem findim_vector_span_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [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 vector_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_findim_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} {p : ι → P} (hi : p) {s : finset ι} {sm : V} [ sm] (hle : (p '' s) sm) (hc : s.card = ) :
(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.

theorem vector_span_eq_of_le_of_affine_independent_of_card_eq_findim_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [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_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_findim_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} {p : ι → P} (hi : p) {s : finset ι} {sp : P} [ (sp.direction)] (hle : (p '' s) sp) (hc : s.card = + 1) :
(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.

theorem affine_span_eq_of_le_of_affine_independent_of_card_eq_findim_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [fintype ι] {p : ι → P} (hi : p) {sp : P} [ (sp.direction)] (hle : (set.range p) sp) (hc : = + 1) :
(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 vector_span_eq_top_of_affine_independent_of_card_eq_findim_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [ 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 affine_span_eq_top_of_affine_independent_of_card_eq_findim_add_one {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [ V] [fintype ι] {p : ι → P} (hi : p) (hc : = ) :

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

theorem findim_vector_span_image_finset_le (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} (p : ι → P) (s : finset ι) {n : } (hc : s.card = n + 1) :
(p '' s)) n

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

theorem findim_vector_span_range_le (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [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_findim_vector_span_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [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_findim_vector_span (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [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_findim_vector_span_le (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [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 findim_vector_span_le_iff_not_affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {ι : Type u_4} [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.

def collinear (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ 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_dim_le_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] (s : set P) :
s s) 1

The definition of collinear.

theorem collinear_iff_findim_le_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ 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_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [field k] [ V] [ P] :

The empty set is collinear.

theorem collinear_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ 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} [field k] [ 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} [field k] [ 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_insert_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ 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} [field k] [ 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} [field k] [ V] [ P] (p : fin 3 → P) :

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