sInf_eq_sInter

Mathlib.Order.SetNotation

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

English

The infimum over a family of sets equals the intersection of that family.

Русский

InfSet семейства множеств равняется пересечению этого семейства.

LaTeX

$$$\mathrm{sInf}\ S = S.\mathrm{sInter}$$$

Lean4

@[simp]
theorem sInf_eq_sInter (S : Set (Set α)) : sInf S = ⋂₀ S :=
  rfl

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

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

Разделы

Аффилиация

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