range_eq_top — Mathlib

English

For a NonUnitalRingHom f, f.range = ⊤ if and only if f is surjective.

Русский

Образ диапазона f равен верхнему подкольцу тогда и только тогда, когда f сюръективен.

LaTeX

$$$f.range = \top \;\iff\; \text{Surjective}(f)$$$

Lean4

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

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