orderIsoOfRightInverse — Mathlib

English

For partial orders α,β, converting a RelIsoLT back to an order isomorphism and back again yields the original RelIsoLT.

Русский

Для частичных порядков α,β преобразование RelIsoLT в OrderIso и обратно возвращает исходный RelIsoLT.

LaTeX

$$$\text{toRelIsoLT}(\text{ofRelIsoLT}(e)) = e$$$

Lean4

/-- A strictly monotone function with a right inverse is an order isomorphism. -/
@[simps -fullyApplied]
def orderIsoOfRightInverse (g : β → α) (hg : Function.RightInverse g f) : α ≃o β :=
  { OrderEmbedding.ofStrictMono f h_mono with toFun := f, invFun := g, left_inv := fun _ => h_mono.injective <| hg _,
    right_inv := hg }

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