sumLexAssoc_symm_apply_inr_inr — Mathlib

English

Let α, β, γ be types with a compatible order. The inverse associativity isomorphism sends inr (inr c) to inr c for all c ∈ γ, i.e. (sumLexAssoc α β γ).symm (inr (inr c)) = inr c.

Русский

Пусть α, β, γ — типы с упорядочиванием. Обратное отображение ассоциативности отправляет inr (inr c) в inr c: (sumLexAssoc α β γ).symm (inr (inr c)) = inr c.

LaTeX

$$$\\bigl(\\text{sumLexAssoc}_{\\alpha,\\beta,\\gamma}\\bigr).symm(\\mathrm{inr}(\\mathrm{inr}(c))) = \\mathrm{inr}(c)$$$

Lean4

@[simp]
theorem sumLexAssoc_symm_apply_inr_inr : (sumLexAssoc α β γ).symm (inr (inr c)) = inr c :=
  rfl

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