mathlib docs: linear_algebra.affine_space.finite

source

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} (h : s.finite) :

finite_dimensional k ↥(vector_span k s)

The vector_span of a finite set is finite-dimensional.

source

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

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

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

source

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

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} [field k] [add_comm_group V] [module k V] [affine_space 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

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

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

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

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 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 : ℕ} (hc : s.card = n + 1) :

finite_dimensional.findim k ↥(vector_span k (p '' ↑s)) = n

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

source

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 : ℕ} (hc : fintype.card ι = n + 1) :

finite_dimensional.findim 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 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] (hle : vector_span k (p '' ↑s) ≤ sm) (hc : s.card = finite_dimensional.findim k ↥sm + 1) :

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

source

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] (hle : vector_span k (set.range p) ≤ sm) (hc : fintype.card ι = finite_dimensional.findim 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_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)] (hle : affine_span k (p '' ↑s) ≤ sp) (hc : s.card = finite_dimensional.findim k ↥(sp.direction) + 1) :

affine_span k (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_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)] (hle : affine_span k (set.range p) ≤ sp) (hc : fintype.card ι = finite_dimensional.findim 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 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} (hi : affine_independent k p) (hc : fintype.card ι = finite_dimensional.findim 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 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} (hi : affine_independent k p) (hc : fintype.card ι = finite_dimensional.findim k V + 1) :

affine_span k (set.range p) = ⊤

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

mathlib documentation

Finite-dimensional subspaces of affine spaces.