orderIsoSumLexPUnit_symm_inr — Mathlib

English

The symmetry of sumLexPUnit on inl maps to some a: (orderIsoSumLexPUnit.symm (toLex (inl a))) = some a.

Русский

Симметрия sumLexPUnit по inl отображает в нечто равное some a: (orderIsoSumLexPUnit.symm (toLex (inl a))) = some a.

LaTeX

$$$\\bigl(\\text{orderIsoSumLexPUnit}^{-1}(\\mathrm{toLex}(\\mathrm{inl}(a)))) = \\mathrm{some}(a)$$$

Lean4

@[simp]
theorem orderIsoSumLexPUnit_symm_inr (x : PUnit) : (@orderIsoSumLexPUnit α _).symm (toLex <| inr x) = ⊤ :=
  rfl

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