sumLexIioIci_symm_apply_Iio — Mathlib

English

The symmetric image of an Iio x element under sumLexIioIci corresponds to toLex of Sum.inl a.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem sumLexIioIci_symm_apply_Iio (a : Iio x) : (sumLexIioIci x).symm a = toLex (Sum.inl a) :=
  sumLexIioIci_symm_apply_of_lt a.2

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