sumLexIicIoi_symm_apply_of_le — Mathlib

English

If y ≤ x, the symmetric evaluation at y lands in the left part via toLex of Sum.inl ⟨y,h⟩.

Русский

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

LaTeX

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

Lean4

theorem sumLexIicIoi_symm_apply_of_le (h : y ≤ x) : (sumLexIicIoi x).symm y = toLex (Sum.inl ⟨y, h⟩) := by
  rw [symm_apply_eq, sumLexIicIoi_apply_inl]

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