coe_iInf

Mathlib.Algebra.Module.Submodule.Lattice

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

← MathLib Explorer

English

The underlying set of the indexed infimum iInf equals the intersection over the index.

Русский

Основание iInf равно пересечению по всем индексам.

LaTeX

$$$\uparrow(\mathrm{iInf}\, p) = \bigcap_{i} \uparrow(p(i))$$$

Lean4

@[simp]
theorem coe_iInf {ι} (p : ι → Submodule R M) : (↑(⨅ i, p i) : Set M) = ⋂ i, ↑(p i) := by rw [iInf, coe_sInf];
  simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

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

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

Разделы

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

Аффилиация

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