English
For a given l and ordinal o, the image under eval of the set {m | m < l} equals the image under πs of the eval set precomposed with π, i.e., images commute with the subdivision by o.
Русский
Для данного l и ординала o множество образов под действием eval совпадает с образом под действием πs от образов eval, полученных после предварительного отображения π и разбиения по o.
LaTeX
$$$\\forall l : Profinite.NobelingProof.Products I\\, \\forall o : Ordinal\\, (hl : \\forall i \\in l.val, ord I i < o)\\n eval C '' \\{m \\mid m < l\\} = (πs C o) '' (eval (π C (ord I · < o)) '' \\{m \\mid m < l\\}).$$
Lean4
theorem eval_πs_image {l : Products I} {o : Ordinal} (hl : ∀ i ∈ l.val, ord I i < o) :
eval C '' {m | m < l} = (πs C o) '' (eval (π C (ord I · < o)) '' {m | m < l}) :=
by
ext f
simp only [Set.mem_image, Set.mem_setOf_eq, exists_exists_and_eq_and]
apply exists_congr; intro m
apply and_congr_right; intro hm
rw [eval_πs C (lt_ord_of_lt hm hl)]
