units_iInf

Mathlib.Algebra.Group.Submonoid.Units

URI: https://scilib.ai/kg/mathlib#Submonoid.units_iInf

English

The units of the infimum of a family of submonoids equal the infimum of the units of each.

Русский

Единицы иInf равны Infimum по компонентам.

LaTeX

$$$ (iInf f).units = \bigwedge_{i} (f i).units $$$

Lean4

@[to_additive]
theorem units_iInf {ι : Sort*} (f : ι → Submonoid M) : (iInf f).units = ⨅ (i : ι), (f i).units :=
  ofUnits_units_gc.u_iInf

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

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

Разделы

Аффилиация

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