English
A different presentation of maximal independence for iUnion of a finite family.
Русский
Другой вариант представления максимальной независимости для iUnion конечной семейства.
LaTeX
$$$\\exists s \\ (\\mathrm{LinearIndependent}_R(v,s) ∧ ∀ t, s ⊆ t ∧ \\mathrm{LinearIndependent}_R(v,t) → s=t)$$$
Lean4
theorem linearIndependent_iUnion_finite {η : Type*} {ιs : η → Type*} {f : ∀ j : η, ιs j → M}
(hindep : ∀ j, LinearIndependent R (f j))
(hd : ∀ i, ∀ t : Set η, t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))) :
LinearIndependent R fun ji : Σ j, ιs j => f ji.1 ji.2 :=
by
nontriviality R
apply LinearIndependent.of_linearIndepOn_id_range
· rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy
by_cases h_cases : x₁ = y₁
· subst h_cases
refine Sigma.eq rfl ?_
rw [LinearIndependent.injective (hindep _) hxy]
· have h0 : f x₁ x₂ = 0 :=
by
apply
disjoint_def.1 (hd x₁ { y₁ } (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h)) (f x₁ x₂)
(subset_span (mem_range_self _))
rw [iSup_singleton]
simp only at hxy
rw [hxy]
exact subset_span (mem_range_self y₂)
exact False.elim ((hindep x₁).ne_zero _ h0)
rw [range_sigma_eq_iUnion_range]
apply linearIndepOn_id_iUnion_finite (fun j => (hindep j).linearIndepOn_id) hd
