valueMonoid_eq_valueGroup'

Mathlib.Algebra.GroupWithZero.Range

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.valueMonoid_eq_valueGroup'

English

The set-valued valueMonoid f equals the underlying set of valueGroup f.

Русский

Множество valueMonoid f равно множеству значений valueGroup f как множества.

LaTeX

$$valueMonoid f = (valueGroup f).toSubmonoid$$

Lean4

theorem valueMonoid_eq_valueGroup' : (valueMonoid f : Set Bˣ) = valueGroup f := by
  rw [valueMonoid_eq_valueGroup, coe_toSubmonoid]

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

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

Разделы

Аффилиация

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