sumLexIicIoi_symm_apply_of_lt — Mathlib

English

If x < y, the symmetric evaluation at y lands in the right part via toLex of Sum.inr ⟨y,h⟩.

Русский

Если x < y, симметричное применение к y попадает в правую часть через toLex( Sum.inr ⟨y,h⟩ ).

LaTeX

$$$ {\\} h : x < y \\;\\Rightarrow\\; (sumLexIicIoi\\, x)^{\\,-1}(y) = toLex(\\text{Sum.inr}\\, ⟨y,h⟩) $$$

Lean4

theorem sumLexIicIoi_symm_apply_of_lt {y : α} (h : x < y) : (sumLexIicIoi x).symm y = toLex (Sum.inr ⟨y, h⟩) := by
  rw [symm_apply_eq, sumLexIicIoi_apply_inr]

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