comp_iff — Mathlib

English

Assuming f is surjective, the following are equivalent: f ≫ g is surjective if and only if g is surjective.

Русский

Полагая, что f сюръективно, тождественно: f ≫ g сюръективно тогда и только тогда, когда g сюръективен.

LaTeX

$$$\mathrm{Surjective}(g_{\mathrm{base}}) \quad\text{iff}\quad \mathrm{Surjective}((f_{\mathrm{base}}) \circ (g_{\mathrm{base}}))$$$

Lean4

theorem comp_iff [Surjective f] : Surjective (f ≫ g) ↔ Surjective g :=
  ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩

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