inter_right_comm — Mathlib

English

Let s1, s2, s3 be finite sets. Then s1 ∩ s2 ∩ s3 = s1 ∩ s3 ∩ s2, i.e., the triple intersection is unchanged by swapping the last two factors.

Русский

Пусть s1, s2, s3 — конечные множества. Тогда s1 ∩ s2 ∩ s3 = s1 ∩ s3 ∩ s2, то есть тройное пересечение не зависит от перестановки двух последних знаменателей.

LaTeX

$$$ (S_1 \cap S_2) \cap S_3 = (S_1 \cap S_3) \cap S_2 $$$

Lean4

theorem inter_right_comm (s₁ s₂ s₃ : Finset α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂ := by grind

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