mapsTo_image — Mathlib

English

If h semiconjugates f with fa and fb and ha maps s to t, then fb maps f''s to f''t.

Русский

Если h полусопряжено между f и fa/ fb и ha отображает s в t, то fb отображает образ f s в образ f t.

LaTeX

$$$h : Semiconj f fa fb \\Rightarrow ha : MapsTo fa s t \\Rightarrow MapsTo fb (f '' s) (f '' t)$$$

Lean4

theorem mapsTo_image (h : Semiconj f fa fb) (ha : MapsTo fa s t) : MapsTo fb (f '' s) (f '' t) := fun _y ⟨x, hx, hy⟩ =>
  hy ▸ ⟨fa x, ha hx, h x⟩

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