range_eq_top — Mathlib

English

Let f: R →+* S be a ring homomorphism. Then the range of f equals the top subring of S if and only if f is surjective.

Русский

Пусть f: R →+* S — гомоморфизм колец. Тогда образ f равен верхнему подкольцу S тогда и только тогда, когда f сюръективен.

LaTeX

$$$ f.\\mathrm{range} = (\\top : \\mathrm{Subring} S) \\iff \\mathrm{Function.Surjective} f $$$

Lean4

theorem range_eq_top {f : R →+* S} : f.range = (⊤ : Subring S) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_range, coe_top]) Set.range_eq_univ

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