sumLexIioIci_symm_apply_of_ge — Mathlib

English

If y lies above x, then the symmetric evaluation map at y corresponds to the inr case of the lex decomposition.

Русский

Если y лежит выше x, то симметричное отображение в y соответствует случаю inr лексического разложения.

LaTeX

$$$ (\\mathrm{sumLexIioIci}\\, x)^{\\,-1}(y) = \\text{toLex}(\\text{Sum.inr}(\\langle y, h\\rangle))$ for $h: x \\le y$$$

Lean4

theorem sumLexIioIci_symm_apply_of_ge {y : α} (h : x ≤ y) : (sumLexIioIci x).symm y = toLex (Sum.inr ⟨y, h⟩) := by
  rw [symm_apply_eq, sumLexIioIci_apply_inr]

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