mapsTo_preimage — Mathlib

English

Let h be a semiconjugacy f fa fb. If MapsTo fb s t holds, then MapsTo fa (f⁻¹'(s)) (f⁻¹'(t)).

Русский

Пусть h является полусопряжением f fa fb. Если fb отображает s в t, тогда fa отображает предобраз f⁻¹'(s) в предобраз f⁻¹'(t).

LaTeX

$$$ (f \\circ fa = fb \\circ f) \\Rightarrow {s t : Set}\\, (\\operatorname{MapsTo} fb s t) \\Rightarrow \\operatorname{MapsTo} fa (f^{-1}' s) (f^{-1}' t). $$$

Lean4

theorem mapsTo_preimage (h : Semiconj f fa fb) {s t : Set β} (hb : MapsTo fb s t) : MapsTo fa (f ⁻¹' s) (f ⁻¹' t) :=
  fun x hx => by simp only [mem_preimage, h x, hb hx]

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