English
Transfinite construction shows linear independence of GoodProducts across all ordinals by induction with Plimit.
Русский
Преобразование по порядку по ординалам демонстрирует линейную независимость GoodProducts по всем ординалам через индукцию и Plimit.
LaTeX
$$$\\forall \\mu : Ordinal, P I \\mu \\Rightarrow\\;\\text{(proof by limit recursion using Plimit and evals).}$$$
Lean4
theorem linearIndependentAux (μ : Ordinal) : P I μ :=
by
refine
Ordinal.limitRecOn μ P0 (fun o h ho C hC hsC ↦ ?_)
(fun o ho h ↦ (GoodProducts.Plimit o ho (fun o' ho' ↦ (h o' ho'))))
have ho' : o < Ordinal.type (· < · : I → I → Prop) := lt_of_lt_of_le (Order.lt_succ _) ho
rw [linearIndependent_iff_sum C hsC ho']
refine ModuleCat.linearIndependent_leftExact (succ_exact C hC hsC ho') ?_ ?_ (succ_mono C o) (square_commutes C ho')
· exact h (le_of_lt ho') (π C (ord I · < o)) (isClosed_proj C o hC) (contained_proj C o)
·
exact
linearIndependent_comp_of_eval C hC hsC ho' (span (π C (ord I · < o)) (isClosed_proj C o hC))
(h (le_of_lt ho') (C' C ho') (isClosed_C' C hC ho') (contained_C' C ho'))
