mrange_eq_top

Mathlib.Algebra.Group.Submonoid.Operations

URI: https://scilib.ai/kg/mathlib#MonoidHom.mrange_eq_top

← MathLib Explorer

English

For any f, mrange f = ⊤ iff f is surjective.

Русский

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

LaTeX

$$$$ \\mathrm{mrange}\,f = \\top \\;\\;\\iff\\;\\; \\mathrm{Surjective}\\;f $$$$

Lean4

@[to_additive]
theorem mrange_eq_top {f : F} : mrange f = (⊤ : Submonoid N) ↔ Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_mrange, coe_top]) Set.range_eq_univ

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru