English
If a product is good with respect to π C (ord I · < o1) and o1 ≤ o2, then it is good with respect to π C (ord I · < o2).
Русский
Если произведение является хорошим относительно π C (ord I · < o1) и o1 ≤ o2, то оно хорошее относительно π C (ord I · < o2).
LaTeX
$$$\\forall l : Profinite.NobelingProof.Products I\\, {o_1 o_2 : Ordinal} (h : o_1 \\le o_2) (hl : l.isGood (π C (ord I · < o_1))) : l.isGood (π C (ord I · < o_2)).$$
Lean4
/-- If `l` is good w.r.t. `π C (ord I · < o₁)` and `o₁ ≤ o₂`, then it is good w.r.t.
`π C (ord I · < o₂)`
-/
theorem isGood_mono {l : Products I} {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂) (hl : l.isGood (π C (ord I · < o₁))) :
l.isGood (π C (ord I · < o₂)) := by
intro hl'
apply hl
rwa [eval_πs_image' C h (prop_of_isGood C _ hl), ← eval_πs' C h (prop_of_isGood C _ hl),
Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C h)] at hl'
