inter_isComm

Mathlib.Data.Set.Basic

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

English

The intersection operation on sets is commutative.

Русский

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

LaTeX

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

Lean4

instance inter_isComm : Std.Commutative (α := Set α) (· ∩ ·) :=
  ⟨inter_comm⟩

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

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

Разделы

Аффилиация

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