instInter

Mathlib.Data.Set.Defs

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

English

There is a binary operation ∩ on Set α defined by s ∩ t = Set.inter s t, i.e., the usual set intersection.

Русский

Существует бинарная операция пересечения на Set α, определённая как s ∩ t = Set.inter s t, то есть обычное пересечение множеств.

LaTeX

$$$\forall s,t \in Set\,\alpha:\ s \cap t \in Set\,\alpha$$$

Lean4

instance : Inter (Set α) :=
  ⟨Set.inter⟩

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

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

Разделы

Аффилиация

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