coe_iInf

Mathlib.Algebra.Group.Subsemigroup.Basic

URI: https://scilib.ai/kg/mathlib#Subsemigroup.coe_iInf

← MathLib Explorer

English

The carrier of the iInf of a family of subsemigroups equals the intersection of their carriers.

Русский

Носитель iInf равен пересечению носителей.

LaTeX

$$$ (\\uparrow( iInf i, S(i) ) : Set M) = \\bigcap_i \\uparrow (S(i))$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_iInf {ι : Sort*} {S : ι → Subsemigroup M} : (↑(⨅ i, S i) : Set M) = ⋂ i, S i := by
  simp only [iInf, coe_sInf, Set.biInter_range]

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

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

Разделы

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

Аффилиация

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