valueMonoid_eq_closure

Mathlib.Algebra.GroupWithZero.Range

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.valueMonoid_eq_closure

English

The valueMonoid of f equals the closure of the preimage of the range of f.

Русский

ValueMonoid f равен замыканию предобраза диапазона f.

LaTeX

$$valueMonoid f = closure ((↑)^{-1}'(range f))$$

Lean4

theorem valueMonoid_eq_closure : valueMonoid f = Submonoid.closure ((↑) ⁻¹' (range f)) :=
  (valueMonoid f).closure_eq.symm

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

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

Разделы

Аффилиация

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