eval_πs — Mathlib

English

Under a hypothesis about ordinals, the evaluation after applying πs to the evaluated π map equals the evaluation on C.

Русский

При условии про ординалов, оценка после применения πs к оцениваемому π-образованию равна оценке на C.

LaTeX

$$$\\text{eval}_{\\pi s}(C,o)(l.eval(π C (ord I·

Lean4

theorem eval_πs {l : Products I} {o : Ordinal} (hlt : ∀ i ∈ l.val, ord I i < o) :
    πs C o (l.eval (π C (ord I · < o))) = l.eval C := by
  simpa only [← LocallyConstant.coe_inj] using evalFacProp C (ord I · < o) hlt

Похожие утверждения