orderIsoOfSurjective — Mathlib

English

A strictly monotone surjective function from a linear order is an order isomorphism.

Русский

Строго монотонная сюръективная функция между линейными порядками является изоморфизмом порядка.

LaTeX

$$(orderIsoOfSurjective f h_mono h_surj) : α ≃o β$$

Lean4

/-- A strictly monotone surjective function from a linear order is an order isomorphism. -/
noncomputable def orderIsoOfSurjective : α ≃o β :=
  (h_mono.orderIso f).trans <| (OrderIso.setCongr _ _ h_surj.range_eq).trans OrderIso.Set.univ

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