Finite-dimensional subspaces of affine spaces.
This file provides a few results relating to finite-dimensional subspaces of affine spaces.
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} :
s.finite → finite_dimensional k ↥(vector_span k s)
The vector_span of a finite set 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} :
s.finite → finite_dimensional k ↥((affine_span k s).direction)
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) :
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.
Equations
- _ = _
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 : ℕ} :
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.
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} :
affine_independent k p → 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
⊤.
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} :
affine_independent k p → 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
⊤.