iInf_eq_iInter

Mathlib.Order.SetNotation

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

English

For a family of sets s, the indexed infimum equals the indexed intersection.

Русский

Для семейства множеств s инфимум равен пересечению по индексу.

LaTeX

$$$\mathrm{iInf}\ s = \mathrm{iInter}\ s$$$

Lean4

@[simp]
theorem iInf_eq_iInter (s : ι → Set α) : iInf s = iInter s :=
  rfl

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

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

Разделы

Аффилиация

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