union_comm_of_disjoint — Mathlib

English

If s1 and s2 are disjoint, then s1 ∪ s2 = s2 ∪ s1.

Русский

Если s1 и s2 несовместимы, то объединение не зависит от порядка: s1 ∪ s2 = s2 ∪ s1.

LaTeX

$$$ s_1 \cup s_2 = s_2 \cup s_1 $$$

Lean4

theorem union_comm_of_disjoint {s₁ s₂ : Finmap β} : Disjoint s₁ s₂ → s₁ ∪ s₂ = s₂ ∪ s₁ :=
  induction_on₂ s₁ s₂ fun s₁ s₂ => by
    intro h
    simp only [AList.toFinmap_eq, union_toFinmap, AList.union_comm_of_disjoint h]

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