English
Another variant form of maximal independence on finite iUnion.
Русский
Еще один вариант максимальной независимости по конечному iUnion.
LaTeX
$$$\\forall i,\\ \\mathrm{LinearIndepOn}_R(id, f(i)) \\Rightarrow \\mathrm{LinearIndepOn}_R(id, \\bigcup i f(i))$$$
Lean4
theorem linearIndepOn_id_iUnion_finite {f : ι → Set M} (hl : ∀ i, LinearIndepOn R id (f i))
(hd : ∀ i, ∀ t : Set ι, t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))) :
LinearIndepOn R id (⋃ i, f i) := by
classical
rw [iUnion_eq_iUnion_finset f]
apply linearIndepOn_iUnion_of_directed
· apply directed_of_isDirected_le
exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h
intro t
induction t using Finset.induction_on with
| empty => simp
| insert i s his ih =>
rw [Finset.set_biUnion_insert]
refine (hl _).id_union ih ?_
rw [span_iUnion₂]
exact hd i s s.finite_toSet his
