mapsTo_image_right — Mathlib

English

If h semiconjugates f fa fb, then MapsTo f s t implies MapsTo f (fa''s) (fb''t).

Русский

Если f полусопряжено между fa и fb, тогда отображение f переносит образы через fa и fb.

LaTeX

$$$(h : Semiconj f fa fb) \\Rightarrow (MapsTo fa s t) \\Rightarrow (MapsTo fb (Set.image f s) (Set.image f t))$$$

Lean4

theorem mapsTo_image_right {t : Set β} (h : Semiconj f fa fb) (hst : MapsTo f s t) : MapsTo f (fa '' s) (fb '' t) :=
  mapsTo_image_iff.2 fun x hx ↦ ⟨f x, hst hx, (h x).symm⟩

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