inter_isAssoc

Mathlib.Data.Set.Basic

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

English

The intersection operation on sets is associative.

Русский

Операция пересечения на множествах ассоциативна.

LaTeX

$$$\text{Inter} \; \text{is associative on } Set\; \alpha$$$

Lean4

instance inter_isAssoc : Std.Associative (α := Set α) (· ∩ ·) :=
  ⟨inter_assoc⟩

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

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

Разделы

Аффилиация

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