mrange_eq_map

Mathlib.Algebra.Group.Submonoid.Operations

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

English

For any f, mrange f equals ⊤.map f.

Русский

Для любого f м_RANGE f совпадает с ⊤.map f.

LaTeX

$$$$ \\mathrm{mrange}\,f = \\top.\\mathrm{map}\,f $$$$

Lean4

@[to_additive]
theorem mrange_eq_map (f : F) : mrange f = (⊤ : Submonoid M).map f :=
  Submonoid.copy_eq _

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

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

Разделы

Аффилиация

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