union_union_union_comm — Mathlib

English

For finite sets s, t, u, v, the fourfold union is invariant under a certain permutation: s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v).

Русский

Для конечных множеств s, t, u, v множество s ∪ t ∪ (u ∪ v) сохраняется при перестановке: s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v).

LaTeX

$$$ s \cup t \cup (u \cup v) = s \cup u \cup (t \cup v) $$$

Lean4

theorem union_union_union_comm (s t u v : Finset α) : s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v) :=
  sup_sup_sup_comm _ _ _ _

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