eq_disjSum_iff — Mathlib

English

Equivalent formulation of the previous fact: u = s ⊎ t iff u^{toLeft} = s and u^{toRight} = t.

Русский

Эквивалентная формулировка предыдущего факта: u = s ⊎ t, если и только если u^{toLeft} = s и u^{toRight} = t.

LaTeX

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

Lean4

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

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