English
If φ is a semiconjugacy from S to T and U is an entourage in Y×Y, then (φ×φ)^{-1}(dynEntourage(T,U,n)) = dynEntourage(S, (φ×φ)^{-1}U, n).
Русский
Если φ является полусопряжением от S к T, и U — окружение в Y×Y, то предобраз dynEntourage(T,U,n) через φ×φ равен dynEntourage(S, предобраз(U) через φ×φ, n).
LaTeX
$$$((\mathrm{map}\,\varphi\,\varphi)^{-1}\' (\mathrm{dynEntourage}(T,U,n)) = \mathrm{dynEntourage}(S,( (\mathrm{map}\,\varphi\,\varphi)^{-1}\' U), n).$$$
Lean4
theorem _root_.Function.Semiconj.preimage_dynEntourage {Y : Type*} {S : X → X} {T : Y → Y} {φ : X → Y}
(h : Function.Semiconj φ S T) (U : Set (Y × Y)) (n : ℕ) :
(map φ φ) ⁻¹' (dynEntourage T U n) = dynEntourage S ((map φ φ) ⁻¹' U) n :=
by
rw [dynEntourage, preimage_iInter₂]
refine iInter₂_congr fun k _ ↦ ?_
rw [← preimage_comp, ← preimage_comp, map_iterate S S k, map_iterate T T k, map_comp_map, map_comp_map,
(Function.Semiconj.iterate_right h k).comp_eq]
