English
There exist a type κ and an injective a: κ → ι such that span_K(v ∘ a) = span_K(v) and v ∘ a is linearly independent.
Русский
Существуют тип κ и инъекция a: κ → ι such that span_K(v ∘ a) = span_K(v) и v ∘ a линейно независимо.
LaTeX
$$$$\exists \kappa \;\exists a:\kappa \to ι,\ Injective(a) \land \operatorname{span}_K(v \circ a) = \operatorname{span}_K(v) \land LinearIndependent_K(v \circ a).$$$$
Lean4
/-- Indexed version of `exists_linearIndependent`. -/
theorem exists_linearIndependent' (v : ι → V) :
∃ (κ : Type u') (a : κ → ι),
Injective a ∧
Submodule.span K (Set.range (v ∘ a)) = Submodule.span K (Set.range v) ∧ LinearIndependent K (v ∘ a) :=
by
obtain ⟨t, ht, hsp, hli⟩ := exists_linearIndependent K (Set.range v)
choose f hf using ht
let s : Set ι := Set.range (fun a : t ↦ f a.property)
have hs {i : ι} (hi : i ∈ s) : v i ∈ t := by obtain ⟨a, rfl⟩ := hi; simp [hf]
let f' (a : s) : t := ⟨v a.val, hs a.property⟩
refine ⟨s, Subtype.val, Subtype.val_injective, hsp.symm ▸ by congr; aesop, ?_⟩
· rw [← show Subtype.val ∘ f' = v ∘ Subtype.val by ext; simp [f']]
apply hli.comp
rintro ⟨i, x, rfl⟩ ⟨j, y, rfl⟩ hij
simp only [Subtype.ext_iff, hf, f'] at hij
simp [hij]
