English
Let f: α → β, fa: α → α, fb: β → β. If fb ∘ f = f ∘ fa and fa is surjective, then fb maps range(f) onto range(f); i.e., every element of range(f) is of the form fb(x) for some x in range(f).
Русский
Пусть f: α → β, fa: α → α, fb: β → β. Если fb ∘ f = f ∘ fa и fa сюръективна, тогда fb отображает range(f) на range(f) сюръективно; то есть каждый элемент диапазона f имеет вид fb(x) для некоторого x ∈ range(f).
LaTeX
$$$ (f \\circ fa = fb \\circ f) \\Rightarrow (\\operatorname{Surjective} fa) \\Rightarrow \\operatorname{SurjOn} fb (\\operatorname{range} f) (\\operatorname{range} f). $$$
Lean4
theorem surjOn_range (h : Semiconj f fa fb) (ha : Surjective fa) : SurjOn fb (range f) (range f) :=
by
rw [← image_univ]
exact h.surjOn_image (ha.surjOn univ)
