sInter

Mathlib.Order.SetNotation

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

English

sInter S is the intersection of a set of sets S: it consists of all elements that belong to every member of S.

Русский

sInter S — пересечение множества множеств S; содержит элементы, принадлежащие каждому члену S.

LaTeX

$$$\mathrm{sInter}\ (S) = \bigcap S$$$

Lean4

/-- Intersection of a set of sets. -/
def sInter (S : Set (Set α)) : Set α :=
  sInf S

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

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

Разделы

Аффилиация

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