disjointSum_comm — Mathlib

English

The disjointSum operation is commutative up to equality: M.disjointSum N h = N.disjointSum M h.symm.

Русский

Операция раздельной суммы коммутативна по смыслу: M.disjointSum N h = N.disjointSum M h.symm.

LaTeX

$$$$ M.disjointSum N h = N.disjointSum M h.symm. $$$$

Lean4

theorem disjointSum_comm {h} : M.disjointSum N h = N.disjointSum M h.symm :=
  by
  ext
  · simp [union_comm]
  repeat
    simpa [union_comm] using
      ⟨fun ⟨m, n, h⟩ ↦ ⟨n, m, M.E.union_comm N.E ▸ h⟩, fun ⟨n, m, h⟩ ↦ ⟨m, n, M.E.union_comm N.E ▸ h⟩⟩

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