orderIso — Mathlib

English

A strictly monotone surjective function from a linear order is an order isomorphism between the domain and its range.

Русский

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

LaTeX

$$$\alpha \cong_o \mathrm{Set.range} f$$$

Lean4

/-- A strictly monotone function from a linear order is an order isomorphism between its domain and
its range. -/
@[simps! apply]
protected noncomputable def orderIso : α ≃o Set.range f
    where
  toEquiv := Equiv.ofInjective f h_mono.injective
  map_rel_iff' := h_mono.le_iff_le

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