sumLexIioIci_symm_apply_Ici — Mathlib

English

The symmetric image of an Ici x element under sumLexIioIci corresponds to toLex of Sum.inr a.

Русский

Симметрическое изображение элемента Ici x под sumLexIioIci соответствует toLex( Sum.inr a ).

LaTeX

$$$ (sumLexIioIci\\, x)^{\\,-1}(a) = \\mathrm{toLex}(\\text{Sum.inr}\\, a)$ for $a \\in \\mathrm{Ici}\\, x$$$

Lean4

@[simp]
theorem sumLexIioIci_symm_apply_Ici (a : Ici x) : (sumLexIioIci x).symm a = toLex (Sum.inr a) :=
  sumLexIioIci_symm_apply_of_ge a.2

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