sumLexAssoc_symm_apply_inr_inl — Mathlib

English

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

Русский

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

LaTeX

$$$\\bigl(\\text{sumLexAssoc}_{\\alpha,\\beta,\\gamma}\\bigr)^{-1}(\\mathrm{inr}(\\mathrm{inl}(b))) = \\mathrm{inl}(\\mathrm{inr}(b))$$$

Lean4

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

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