surjective_comp — Mathlib

English

Let e be a surjective map in an EquivLike-like setting and f any map; then f ∘ e is surjective if and only if f is surjective.

Русский

Пусть e сюръективно отображает множества в контексте EquivLike, и пусть f — произвольное отображение; тогда f ∘ e сюръективно тогда и только тогда, когда сюръективен f.

LaTeX

$$$\text{Surjective}(e) \rightarrow \big(\text{Surjective}(f \circ e) \iff \text{Surjective}(f)\big)$$$

Lean4

@[simp]
theorem surjective_comp (e : E) (f : β → γ) : Function.Surjective (f ∘ e) ↔ Function.Surjective f :=
  (EquivLike.surjective e).of_comp_iff f

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