English
Let l be a product in the Nobeling construction over I, and let o1 ≤ o2 be ordinals. If every coordinate i in l.val satisfies ord I i < o1, then applying the πs' map with bound o1 and evaluating l at the projection π C (ord I · < o1) yields the same result as evaluating l at π C (ord I · < o2).
Русский
Пусть l — элемент произведения в конструировании Nobeling над I, и пусть o1 ≤ o2 — ординалы. Если для каждого координатного индекса i из l.val верно ord I i < o1, то применение отображения πs' с верхней границей o1 к l.eval(π C(ord I · < o1)) даёт такой же результат, как и l.eval(π C(ord I · < o2)).
LaTeX
$$$\\forall I\\, C\\, [\\text{LinearOrder } I]\, [\\text{WellFoundedLT } I]\\, {l : Profinite.NobelingProof.Products I} {o_1 o_2 : Ordinal},\\ (h : o_1 \\le o_2)\\ (hlt : \\forall i \\in l.val, \\ ord I i < o_1)\\Rightarrow \n \\pi_s' C h \\left(l.eval \\left(\\pi C(\\operatorname{ord} I \\cdot < o_1)\\right)\\right) = l.eval \\left(\\pi C(\\operatorname{ord} I \\cdot < o_2)\\right).$$
Lean4
theorem eval_πs' {l : Products I} {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂) (hlt : ∀ i ∈ l.val, ord I i < o₁) :
πs' C h (l.eval (π C (ord I · < o₁))) = l.eval (π C (ord I · < o₂)) :=
by
rw [← LocallyConstant.coe_inj, ← LocallyConstant.toFun_eq_coe]
exact evalFacProps C (fun (i : I) ↦ ord I i < o₁) (fun (i : I) ↦ ord I i < o₂) hlt (fun _ hh ↦ lt_of_lt_of_le hh h)
