toLexRelIsoLE_symm_coe — Mathlib

English

The inverse of the LE RelIso mapping between Sum.Lex and α ⊕β is the ofLex map, making the isomorphism symmetric with respect to the order.

Русский

Обратное отображение LE RelIso между Sum.Lex и α ⊕ β совпадает с отображением ofLex, образуя симметрию между порядками.

LaTeX

$$$\\bigl\\{ toLexRelIsoLE \\bigr\\}^{-1} = ofLex$$$

Lean4

@[simp]
theorem toLexRelIsoLE_symm_coe [LE α] [LE β] : ⇑(toLexRelIsoLE (α := α) (β := β)).symm = ofLex :=
  rfl

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