iInter

Mathlib.Order.SetNotation

URI: https://scilib.ai/kg/mathlib#Set.iInter

English

iInter takes the intersection over a family indexed by i, i.e., the infimum of sets s(i) over i.

Русский

iInter берет пересечение по индексовой семье i, то есть инфимум множеств s(i).

LaTeX

$$$\mathrm{iInter}\ (s) = iInf\, s$$$

Lean4

/-- Indexed intersection of a family of sets -/
def iInter (s : ι → Set α) : Set α :=
  iInf s

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

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

Разделы

Аффилиация

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