disjSum_eq_iff — Mathlib

English

A disjoint sum equality characterizes a decomposition: s ⊎ t = u if and only if u^{toLeft} = s and u^{toRight} = t.

Русский

Равенство дизъюнктной суммы характеризует разложение: s ⊎ t = u эквивалентно u^{toLeft} = s и u^{toRight} = t.

LaTeX

$$s \uplus t = u \iff u^{\mathrm{toLeft}} = s \land u^{\mathrm{toRight}} = t$$

Lean4

theorem disjSum_eq_iff : s.disjSum t = u ↔ s = u.toLeft ∧ t = u.toRight :=
  ⟨fun h => by simp [← h], fun h => by simp [h, toLeft_disjSum_toRight]⟩

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