of_comp — Mathlib

English

Let h : SurjOn (g ∘ f) s p and hr : MapsTo f s t. Then g is surjective from t onto p.

Русский

Пусть h : SurjOn (g ∘ f) s p и hr : MapsTo f s t. Тогда отображение g отображает множество t поверх p.

LaTeX

$$$ (\mathrm{SurjOn}(g\circ f) s p) \land (\mathrm{MapsTo} f s t) \rightarrow \mathrm{SurjOn} g t p $$$

Lean4

theorem of_comp (h : SurjOn (g ∘ f) s p) (hr : MapsTo f s t) : SurjOn g t p :=
  by
  intro z hz
  obtain ⟨x, hx, rfl⟩ := h hz
  exact ⟨f x, hr hx, rfl⟩

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