English
Under the same assumptions as eval_πs_image, the equality also holds with the roles of the two π-preimages swapped, relating eval with πs' and the corresponding projections.
Русский
При тех же предпосылках, что и в eval_πs_image, выполняется тождество при поменных ролях между eval и πs', отображающее соответствия между отображениями и проекциями.
LaTeX
$$$\\forall l : Profinite.NobelingProof.Products I\\, \\forall o_1 o_2 : Ordinal\\, (h : o_1 \\le o_2)\\ (hl : ∀ i ∈ l.val, ord I i < o_1)\\n eval (π C (ord I · < o_2)) '' {m | m < l} = (πs' C h) '' (eval (π C (ord I · < o_1)) '' {m | m < l}).$$
Lean4
theorem eval_πs_image' {l : Products I} {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂) (hl : ∀ i ∈ l.val, ord I i < o₁) :
eval (π C (ord I · < o₂)) '' {m | m < l} = (πs' C h) '' (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 h (lt_ord_of_lt hm hl)]
