coe_iInf

Mathlib.Algebra.Group.Subgroup.Lattice

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

← MathLib Explorer

English

The underlying set of the infimum over a family (iInf) equals the intersection over indices.

Русский

Множество, лежащее в основании iInf, равно ⋂ i, S_i.

LaTeX

$$$(↑(\iInf i, S i) : Set G) = \bigcap_i S_i$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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