inter_assoc

Mathlib.Data.Set.Basic

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

English

For sets a, b, c, the intersection is associative: a ∩ b ∩ c = a ∩ (b ∩ c).

Русский

Для множеств A, B, C пересечение является ассоциативным: A ∩ B ∩ C = A ∩ (B ∩ C).

LaTeX

$$$a \cap b \cap c = a \cap (b \cap c)$$$

Lean4

theorem inter_assoc (a b c : Set α) : a ∩ b ∩ c = a ∩ (b ∩ c) :=
  ext fun _ => and_assoc

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

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

Разделы

Аффилиация

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