surjective_respectsIso — Mathlib

English

Surjectivity respects isomorphisms: surjectivity is preserved under isomorphisms.

Русский

Суръективность сохраняется при изоморфизмах: суръективность сохраняется под изоморфизмами.

LaTeX

$$$$ \operatorname{RespectsIso}(\mathrm{surjective}). $$$$

Lean4

theorem surjective_respectsIso : RespectsIso surjective :=
  by
  apply surjective_stableUnderComposition.respectsIso
  intro _ _ _ _ e
  exact e.surjective

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