sumAssoc_symm_apply_inr_inl — Mathlib

English

The inverse map sends inr(inl b) to inl(inr b): (sumAssoc α β γ).symm (inr (inl b)) = inl (inr b).

Русский

Обратное отображение отправляет inr(inl b) в inl(inr b): (sumAssoc α β γ).symm (inr (inl b)) = inl (inr b).

LaTeX

$$$ (\text{sumAssoc }(\alpha,\beta,\gamma)).\mathrm{symm} (\mathrm{inr}(\mathrm{inl} b)) = \mathrm{inl}(\mathrm{inr} b) $$$

Lean4

@[simp]
theorem sumAssoc_symm_apply_inr_inl : (sumAssoc α β γ).symm (inr (inl b)) = inl (inr b) :=
  rfl

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