comp_right — Mathlib

English

If f is surjective and g maps s onto t, then g ∘ f maps f⁻¹'(s) onto t.

Русский

Если f сюръективна, а g отображает s на t, то g ∘ f отображает f⁻¹'(s) на t.

LaTeX

$$$ \mathrm{SurjOn} f s t \land \mathrm{Surjective} f \rightarrow \mathrm{SurjOn}(g\circ f) (f^{-1}'s) t $$$

Lean4

theorem comp_right {s : Set β} {t : Set γ} (hf : Surjective f) (hg : SurjOn g s t) : SurjOn (g ∘ f) (f ⁻¹' s) t := by
  rwa [SurjOn, image_comp g f, image_preimage_eq _ hf]

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