surjOn_image — Mathlib

English

If h is a semiconjugacy, then MapsTo f s t yields MapsTo f (image fa s) (image fb t).

Русский

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

LaTeX

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

Lean4

theorem surjOn_image (h : Semiconj f fa fb) (ha : SurjOn fa s t) : SurjOn fb (f '' s) (f '' t) :=
  by
  rintro y ⟨x, hxt, rfl⟩
  rcases ha hxt with ⟨x, hxs, rfl⟩
  rw [h x]
  exact mem_image_of_mem _ (mem_image_of_mem _ hxs)

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