srange_eq_top_iff_surjective — Mathlib

English

For any f, srange f = ⊤ if and only if f is surjective.

Русский

Для любого f образ srange f равен ⊤ тогда и только тогда, когда f сюръективен.

LaTeX

$$$ srange f = \top \;\Leftrightarrow\; Function.Surjective f$$

Lean4

theorem srange_eq_top_iff_surjective {f : F} :
    srange f = (⊤ : NonUnitalSubsemiring S) ↔ Function.Surjective (f : R → S) :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_srange, coe_top]) Set.range_eq_univ

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