mathlib documentation

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

theorem finite_dimensional_vector_span_of_finite (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [add_comm_group V] [module k V] [affine_space V P] {s : set P} :

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] [add_comm_group V] [module k V] [affine_space 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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] (p : ι → P) (s : set ι) :

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] [add_comm_group V] [module k V] [affine_space V P] {s : set P} :

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] [add_comm_group V] [module k V] [affine_space 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] [add_comm_group V] [module k V] [affine_space 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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {p : ι → P} (hi : affine_independent k p) {s : finset ι} {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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] {p : ι → P} (hi : affine_independent k p) {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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sm : submodule k V} [finite_dimensional k sm] :
vector_span k (p '' s) sms.card = finite_dimensional.findim k sm + 1vector_span k (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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] {p : ι → P} (hi : affine_independent k p) {sm : submodule k V} [finite_dimensional k 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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sp : affine_subspace k P} [finite_dimensional k (sp.direction)] :

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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] {p : ι → P} (hi : affine_independent k p) {sp : affine_subspace k P} [finite_dimensional k (sp.direction)] :

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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [finite_dimensional k V] [fintype ι] {p : ι → P} :

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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [finite_dimensional k V] [fintype ι] {p : ι → P} :

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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} (p : ι → P) (s : finset ι) {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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] (p : ι → P) {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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] (p : ι → P) {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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] (p : ι → P) {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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] (p : ι → P) {n : } :

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] [add_comm_group V] [module k V] [affine_space V P] {ι : Type u_4} [fintype ι] (p : ι → P) {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] [add_comm_group V] [module k V] [affine_space V P] :
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] [add_comm_group V] [module k V] [affine_space V P] (s : set P) :

The definition of collinear.

theorem collinear_iff_findim_le_one (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [add_comm_group V] [module k V] [affine_space V P] (s : set P) [finite_dimensional k (vector_span k s)] :

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

The empty set is collinear.

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

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