surjOn_comp_iff — Mathlib

English

The surjectivity of a composition is equivalent to the surjectivity of g on the image of f.

Русский

Сюръекция композиции эквивалентна сюръекции функции g на образе f.

LaTeX

$$$ \mathrm{SurjOn}(g\circ f) s p \;\iff\; \mathrm{SurjOn} g (f''s) p $$$

Lean4

theorem surjOn_comp_iff : SurjOn (g ∘ f) s p ↔ SurjOn g (f '' s) p :=
  ⟨fun h ↦ h.of_comp <| mapsTo_image f s, fun h ↦ h.comp <| surjOn_image _ _⟩

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