English
Define P(o) to be the property that if o ≤ type(<) and C is closed, and C is contained in o, then the ℤ-linear independence holds for GoodProducts.eval C.
Русский
Определим P(o) как свойство: если o ≤ type(<) и C замкнуто, и C содержится в o, тогда GoodProducts.eval C линейно независимо над ℤ.
LaTeX
$$$P(o) := o \\le \\mathrm{type}((<)) \\;\\Rightarrow\\; (\\forall C, \\ IsClosed C \\to \\mathrm{contained}(C,o)\\to \\mathrm{LinearIndependent}_{\\mathbb{Z}}(\\mathrm{GoodProducts.eval} C)).$$$
Lean4
/-- The predicate on ordinals which we prove by induction, see `GoodProducts.P0`,
`GoodProducts.Plimit` and `GoodProducts.linearIndependentAux` in the section `Induction` below
-/
def P (o : Ordinal) : Prop :=
o ≤ Ordinal.type (· < · : I → I → Prop) →
(∀ (C : Set (I → Bool)), IsClosed C → contained C o → LinearIndependent ℤ (GoodProducts.eval C))
