Linear independence #
This file collects consequences of linear (in)dependence and includes specialized tests for specific families of vectors, requiring more theory to state.
Main statements #
We prove several specialized tests for linear independence of families of vectors and of sets of vectors.
linearIndependent_option,linearIndependent_fin_cons,linearIndependent_fin_succ: type-specific tests for linear independence of families of vector fields;linearIndependent_insert,linearIndependent_pair: linear independence tests for set operations
In many cases we additionally provide dot-style operations (e.g., LinearIndependent.union) to
make the linear independence tests usable as hv.insert ha etc.
We also prove that, when working over a division ring, any family of vectors includes a linear independent subfamily spanning the same subspace.
TODO #
Rework proofs to hold in semirings, by avoiding the path through
ker (Finsupp.linearCombination R v) = ⊥.
Tags #
linearly dependent, linear dependence, linearly independent, linear independence
theorem
Fintype.linearIndependent_iff'ₛ
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Fintype ι]
[DecidableEq ι]
:
LinearIndependent R v ↔ Function.Injective ⇑((LinearMap.lsum R (fun (x : ι) => R) ℕ) fun (i : ι) => LinearMap.id.smulRight (v i))
A finite family of vectors v i is linear independent iff the linear map that sends
c : ι → R to ∑ i, c i • v i is injective.
theorem
linearIndepOn_iUnion_of_directed
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{η : Type u_6}
{s : η → Set ι}
(hs : Directed (fun (x1 x2 : Set ι) => x1 ⊆ x2) s)
(h : ∀ (i : η), LinearIndepOn R v (s i))
:
LinearIndepOn R v (⋃ (i : η), s i)
@[deprecated linearIndepOn_iUnion_of_directed (since := "2025-02-15")]
theorem
linearIndependent_iUnion_of_directed
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{η : Type u_6}
{s : η → Set ι}
(hs : Directed (fun (x1 x2 : Set ι) => x1 ⊆ x2) s)
(h : ∀ (i : η), LinearIndepOn R v (s i))
:
LinearIndepOn R v (⋃ (i : η), s i)
Alias of linearIndepOn_iUnion_of_directed.
theorem
linearIndepOn_sUnion_of_directed
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set (Set ι)}
(hs : DirectedOn (fun (x1 x2 : Set ι) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, LinearIndepOn R v a)
:
LinearIndepOn R v (⋃₀ s)
@[deprecated linearIndepOn_sUnion_of_directed (since := "2025-02-15")]
theorem
linearIndependent_sUnion_of_directed
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set (Set ι)}
(hs : DirectedOn (fun (x1 x2 : Set ι) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, LinearIndepOn R v a)
:
LinearIndepOn R v (⋃₀ s)
Alias of linearIndepOn_sUnion_of_directed.
theorem
linearIndepOn_biUnion_of_directed
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{η : Type u_6}
{s : Set η}
{t : η → Set ι}
(hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set ι) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, LinearIndepOn R v (t a))
:
LinearIndepOn R v (⋃ a ∈ s, t a)
@[deprecated linearIndepOn_biUnion_of_directed (since := "2025-02-15")]
theorem
linearIndependent_biUnion_of_directed
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{η : Type u_6}
{s : Set η}
{t : η → Set ι}
(hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set ι) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, LinearIndepOn R v (t a))
:
LinearIndepOn R v (⋃ a ∈ s, t a)
Alias of linearIndepOn_biUnion_of_directed.
theorem
LinearIndependent.iSupIndep_span_singleton
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(hv : LinearIndependent R v)
:
iSupIndep fun (i : ι) => Submodule.span R {v i}
See also iSupIndep_iff_linearIndependent_of_ne_zero.
@[deprecated LinearIndependent.iSupIndep_span_singleton (since := "2024-11-24")]
theorem
LinearIndependent.independent_span_singleton
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(hv : LinearIndependent R v)
:
iSupIndep fun (i : ι) => Submodule.span R {v i}
Alias of LinearIndependent.iSupIndep_span_singleton.
See also iSupIndep_iff_linearIndependent_of_ne_zero.
theorem
linearIndependent_inl_union_inr'
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M']
[Module R M]
[Module R M']
{v : ι → M}
{v' : ι' → M'}
(hv : LinearIndependent R v)
(hv' : LinearIndependent R v')
:
LinearIndependent R (Sum.elim (⇑(LinearMap.inl R M M') ∘ v) (⇑(LinearMap.inr R M M') ∘ v'))
theorem
LinearIndependent.inl_union_inr
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M']
[Module R M]
[Module R M']
{s : Set M}
{t : Set M'}
(hs : LinearIndependent R fun (x : ↑s) => ↑x)
(ht : LinearIndependent R fun (x : ↑t) => ↑x)
:
LinearIndependent R fun (x : ↑(⇑(LinearMap.inl R M M') '' s ∪ ⇑(LinearMap.inr R M M') '' t)) => ↑x
theorem
exists_maximal_linearIndepOn'
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(v : ι → M)
:
∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
TODO : refactor to use Maximal.
@[deprecated exists_maximal_linearIndepOn' (since := "2025-02-15")]
theorem
exists_maximal_independent'
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(v : ι → M)
:
∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
Alias of exists_maximal_linearIndepOn'.
TODO : refactor to use Maximal.
theorem
Fintype.linearIndependent_iff'
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Fintype ι]
[DecidableEq ι]
:
LinearIndependent R v ↔ LinearMap.ker ((LinearMap.lsum R (fun (x : ι) => R) ℕ) fun (i : ι) => LinearMap.id.smulRight (v i)) = ⊥
A finite family of vectors v i is linear independent iff the linear map that sends
c : ι → R to ∑ i, c i • v i has the trivial kernel.
theorem
LinearIndependent.pair_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
Also see LinearIndependent.pair_iff' for a simpler version over fields.
theorem
LinearIndependent.pair_symm_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
@[simp]
theorem
LinearIndependent.pair_neg_left_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
@[simp]
theorem
LinearIndependent.pair_neg_right_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
theorem
LinearIndependent.pair_smul_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[NoZeroSMulDivisors S R]
{u : S}
(hu : u ≠ 0)
:
@[simp]
theorem
LinearIndependent.pair_add_smul_add_smul_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[NoZeroSMulDivisors S R]
(a b c d : S)
[Nontrivial R]
:
@[deprecated LinearIndependent.pair_add_smul_add_smul_iff (since := "2025-04-15")]
theorem
LinearIndependent.linear_combination_pair_of_det_ne_zero
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[NoZeroSMulDivisors S R]
(a b c d : S)
[Nontrivial R]
:
@[simp]
theorem
LinearIndependent.pair_add_smul_right_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[NoZeroSMulDivisors S R]
(c : S)
:
@[simp]
theorem
LinearIndependent.pair_add_smul_left_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
{S : Type u_6}
[CommRing S]
[Module S R]
[Module S M]
[SMulCommClass S R M]
[IsScalarTower S R M]
[NoZeroSMulDivisors S R]
(b : S)
:
@[simp]
theorem
LinearIndependent.pair_add_right_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
@[simp]
theorem
LinearIndependent.pair_add_left_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x y : M}
:
theorem
linearIndepOn_id_iUnion_finite
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{f : ι → Set M}
(hl : ∀ (i : ι), LinearIndepOn R id (f i))
(hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (Submodule.span R (f i)) (⨆ i ∈ t, Submodule.span R (f i)))
:
LinearIndepOn R id (⋃ (i : ι), f i)
@[deprecated linearIndepOn_id_iUnion_finite (since := "2025-02-15")]
theorem
linearIndependent_iUnion_finite_subtype
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{f : ι → Set M}
(hl : ∀ (i : ι), LinearIndepOn R id (f i))
(hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (Submodule.span R (f i)) (⨆ i ∈ t, Submodule.span R (f i)))
:
LinearIndepOn R id (⋃ (i : ι), f i)
Alias of linearIndepOn_id_iUnion_finite.
theorem
linearIndependent_iUnion_finite
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{η : Type u_6}
{ιs : η → Type u_7}
{f : (j : η) → ιs j → M}
(hindep : ∀ (j : η), LinearIndependent R (f j))
(hd :
∀ (i : η) (t : Set η),
t.Finite → i ∉ t → Disjoint (Submodule.span R (Set.range (f i))) (⨆ i ∈ t, Submodule.span R (Set.range (f i))))
:
LinearIndependent R fun (ji : (j : η) × ιs j) => f ji.fst ji.snd
theorem
exists_maximal_linearIndepOn
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(v : ι → M)
:
∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ a • v i ∈ Submodule.span R (v '' s)
@[deprecated exists_maximal_linearIndepOn (since := "2025-02-15")]
theorem
exists_maximal_independent
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(v : ι → M)
:
∃ (s : Set ι), LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ (a : R), a ≠ 0 ∧ a • v i ∈ Submodule.span R (v '' s)
Alias of exists_maximal_linearIndepOn.
theorem
linearIndependent_algHom_toLinearMap
(K : Type u_6)
(M : Type u_7)
(L : Type u_8)
[CommSemiring K]
[Semiring M]
[Algebra K M]
[CommRing L]
[IsDomain L]
[Algebra K L]
:
Properties which require DivisionRing K #
These can be considered generalizations of properties of linear independence in vector spaces.
theorem
mem_span_insert_exchange
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x y : V}
:
x ∈ Submodule.span K (insert y s) → x ∉ Submodule.span K s → y ∈ Submodule.span K (insert x s)
theorem
LinearIndepOn.insert
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x : V}
(hs : LinearIndepOn K id s)
(hx : x ∉ Submodule.span K s)
:
LinearIndepOn K id (insert x s)
@[deprecated LinearIndepOn.insert (since := "2025-02-15")]
theorem
LinearIndependent.insert
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x : V}
(hs : LinearIndepOn K id s)
(hx : x ∉ Submodule.span K s)
:
LinearIndepOn K id (Insert.insert x s)
Alias of LinearIndepOn.insert.
theorem
linearIndependent_option'
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{x : V}
:
(LinearIndependent K fun (o : Option ι) => o.casesOn' x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
theorem
LinearIndependent.option
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{x : V}
(hv : LinearIndependent K v)
(hx : x ∉ Submodule.span K (Set.range v))
:
LinearIndependent K fun (o : Option ι) => o.casesOn' x v
theorem
linearIndependent_option
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : Option ι → V}
:
LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ v none ∉ Submodule.span K (Set.range (v ∘ some))
theorem
linearIndepOn_insert
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
(has : a ∉ s)
:
@[deprecated linearIndepOn_insert (since := "2025-02-15")]
theorem
linearIndependent_insert'
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
(has : a ∉ s)
:
Alias of linearIndepOn_insert.
theorem
linearIndepOn_id_insert
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x : V}
(hxs : x ∉ s)
:
@[deprecated linearIndepOn_insert (since := "2025-02-15")]
theorem
linearIndependent_insert
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
(has : a ∉ s)
:
Alias of linearIndepOn_insert.
theorem
linearIndepOn_insert_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
:
theorem
linearIndepOn_id_insert_iff
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{a : V}
{s : Set V}
:
theorem
LinearIndepOn.mem_span_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
(h : LinearIndepOn K f s)
:
theorem
LinearIndepOn.notMem_span_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
(h : LinearIndepOn K f s)
:
A shortcut to a convenient form for the negation in LinearIndepOn.mem_span_iff.
@[deprecated LinearIndepOn.notMem_span_iff (since := "2025-05-23")]
theorem
LinearIndepOn.not_mem_span_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set ι}
{a : ι}
{f : ι → V}
(h : LinearIndepOn K f s)
:
Alias of LinearIndepOn.notMem_span_iff.
A shortcut to a convenient form for the negation in LinearIndepOn.mem_span_iff.
theorem
LinearIndepOn.mem_span_iff_id
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{a : V}
(h : LinearIndepOn K id s)
:
theorem
LinearIndepOn.notMem_span_iff_id
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{a : V}
(h : LinearIndepOn K id s)
:
@[deprecated LinearIndepOn.notMem_span_iff_id (since := "2025-05-23")]
theorem
LinearIndepOn.not_mem_span_iff_id
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{a : V}
(h : LinearIndepOn K id s)
:
Alias of LinearIndepOn.notMem_span_iff_id.
theorem
linearIndepOn_id_pair
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x y : V}
(hx : x ≠ 0)
(hy : ∀ (a : K), a • x ≠ y)
:
LinearIndepOn K id {x, y}
@[deprecated linearIndepOn_id_pair (since := "2025-02-15")]
theorem
linearIndependent_pair
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x y : V}
(hx : x ≠ 0)
(hy : ∀ (a : K), a • x ≠ y)
:
LinearIndepOn K id {x, y}
Alias of linearIndepOn_id_pair.
theorem
linearIndepOn_pair_iff
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{i j : ι}
(v : ι → V)
(hij : i ≠ j)
(hi : v i ≠ 0)
:
LinearIndepOn.pair_iff is a version that works over arbitrary rings.
theorem
LinearIndependent.pair_iff'
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x y : V}
(hx : x ≠ 0)
:
Also see LinearIndependent.pair_iff for the version over arbitrary rings.
theorem
linearIndependent_fin_cons
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{n : ℕ}
{v : Fin n → V}
:
theorem
linearIndependent_fin_snoc
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{n : ℕ}
{v : Fin n → V}
:
theorem
LinearIndependent.fin_cons
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{n : ℕ}
{v : Fin n → V}
(hv : LinearIndependent K v)
(hx : x ∉ Submodule.span K (Set.range v))
:
LinearIndependent K (Fin.cons x v)
See LinearIndependent.fin_cons' for an uglier version that works if you
only have a module over a semiring.
theorem
linearIndependent_fin_succ
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
{v : Fin (n + 1) → V}
:
LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (Set.range (Fin.tail v))
theorem
linearIndependent_fin_succ'
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
{v : Fin (n + 1) → V}
:
LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ Submodule.span K (Set.range (Fin.init v))
def
equiv_linearIndependent
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(n : ℕ)
:
Equivalence between k + 1 vectors of length n and k vectors of length n along with a
vector in the complement of their span.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
linearIndependent_fin2
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{f : Fin 2 → V}
:
theorem
exists_linearIndepOn_id_extension
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndepOn K id b
TODO : generalize this and related results to non-identity functions
@[deprecated exists_linearIndepOn_id_extension (since := "2025-02-15")]
theorem
exists_linearIndependent_extension
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndepOn K id b
Alias of exists_linearIndepOn_id_extension.
TODO : generalize this and related results to non-identity functions
theorem
exists_linearIndependent
(K : Type u_3)
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(t : Set V)
:
∃ b ⊆ t, Submodule.span K b = Submodule.span K t ∧ LinearIndependent K Subtype.val
theorem
exists_linearIndependent'
{ι : Type u'}
(K : Type u_3)
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(v : ι → V)
:
∃ (κ : Type u') (a : κ → ι),
Function.Injective a ∧ Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧ LinearIndependent K (v ∘ a)
Indexed version of exists_linearIndependent.
noncomputable def
LinearIndepOn.extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
Set V
LinearIndepOn.extend adds vectors to a linear independent set s ⊆ t until it spans
all elements of t.
TODO - generalize the lemmas below to functions that aren't the identity.
Equations
- hs.extend hst = Classical.choose ⋯
Instances For
@[deprecated LinearIndepOn.extend (since := "2025-02-15")]
def
LinearIndependent.extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
Set V
Alias of LinearIndepOn.extend.
LinearIndepOn.extend adds vectors to a linear independent set s ⊆ t until it spans
all elements of t.
TODO - generalize the lemmas below to functions that aren't the identity.
Equations
Instances For
theorem
LinearIndepOn.extend_subset
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
@[deprecated LinearIndepOn.extend_subset (since := "2025-02-15")]
theorem
LinearIndependent.extend_subset
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
Alias of LinearIndepOn.extend_subset.
theorem
LinearIndepOn.subset_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
@[deprecated LinearIndepOn.subset_extend (since := "2025-02-15")]
theorem
LinearIndependent.subset_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
Alias of LinearIndepOn.subset_extend.
theorem
LinearIndepOn.subset_span_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
@[deprecated LinearIndepOn.subset_span_extend (since := "2025-02-15")]
theorem
LinearIndependent.subset_span_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
Alias of LinearIndepOn.subset_span_extend.
theorem
LinearIndepOn.span_extend_eq_span
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
@[deprecated LinearIndepOn.span_extend_eq_span (since := "2025-02-15")]
theorem
LinearIndependent.span_extend_eq_span
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
Alias of LinearIndepOn.span_extend_eq_span.
theorem
LinearIndepOn.linearIndepOn_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
LinearIndepOn K id (hs.extend hst)
@[deprecated LinearIndepOn.linearIndepOn_extend (since := "2025-02-15")]
theorem
LinearIndependent.linearIndependent_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ t)
:
LinearIndepOn K id (hs.extend hst)
Alias of LinearIndepOn.linearIndepOn_extend.
theorem
exists_of_linearIndepOn_of_finite_span
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Finset V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ ↑(Submodule.span K ↑t))
:
@[deprecated exists_of_linearIndepOn_of_finite_span (since := "2025-02-15")]
theorem
exists_of_linearIndependent_of_finite_span
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Finset V}
(hs : LinearIndepOn K id s)
(hst : s ⊆ ↑(Submodule.span K ↑t))
:
Alias of exists_of_linearIndepOn_of_finite_span.
theorem
exists_finite_card_le_of_finite_of_linearIndependent_of_span
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s t : Set V}
(ht : t.Finite)
(hs : LinearIndepOn K id s)
(hst : s ⊆ ↑(Submodule.span K t))
: