mrange_eq_top_of_surjective — Mathlib

English

If f is surjective, then mrange f = ⊤.

Русский

Если f сюръективен, то mrange f = ⊤.

LaTeX

$$$$ \\mathrm{Surjective}\\;f \\Rightarrow \\mathrm{mrange}\;f = \\top $$$$

Lean4

/-- The range of a surjective monoid hom is the whole of the codomain. -/
@[to_additive (attr := simp) /-- The range of a surjective `AddMonoid` hom is the whole of the codomain. -/
    ]
theorem mrange_eq_top_of_surjective (f : F) (hf : Function.Surjective f) : mrange f = (⊤ : Submonoid N) :=
  mrange_eq_top.2 hf

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