English
GoodProducts Basis provides a ℤ-basis for LocallyConstant C ℤ, built from linear independence and span.
Русский
База GoodProducts задаёт ℤ-базис для LocallyConstant C ℤ, строят её из линейной независимости и порождающего подпространства.
LaTeX
$$$\\text{Basis }(hC) :\\,\\text{Basis }(GoodProducts C)\\,\\mathbb{Z}\\,\\text{LocallyConstant } C\\mathbb{Z} = \\text{Basis.mk} (GoodProducts.linearIndependent C hC) (GoodProducts.span C hC)$$$
Lean4
theorem Plimit (o : Ordinal) (ho : Order.IsSuccLimit o) : (∀ (o' : Ordinal), o' < o → P I o') → P I o :=
by
intro h hho C hC hsC
rw [linearIndependent_iff_union_smaller C ho hsC, linearIndependent_subtype_iff]
exact
linearIndepOn_iUnion_of_directed (Monotone.directed_le fun _ _ h ↦ GoodProducts.smaller_mono C h) fun ⟨o', ho'⟩ ↦
(linearIndependent_iff_smaller _ _).mp
(h o' ho' (ho'.le.trans hho) (π C (ord I · < o')) (isClosed_proj _ _ hC) (contained_proj _ _))
