range_eq_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem range_eq_top {f : M →[L] N} : range f = ⊤ ↔ Function.Surjective f := by
  rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_eq_univ]

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