inter_assoc

Mathlib.Data.Finset.Lattice.Basic

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

English

Intersection is associative: S1 ∩ S2 ∩ S3 = S1 ∩ (S2 ∩ S3).

Русский

Пересечение ассоциативно: S1 ∩ S2 ∩ S3 = S1 ∩ (S2 ∩ S3).

LaTeX

$$$s_{1} \\cap s_{2} \\cap s_{3} = s_{1} \\cap (s_{2} \\cap s_{3})$$$

Lean4

@[simp]
theorem inter_assoc (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) := by grind

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

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

Разделы

Аффилиация

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