English
If f is strictly monotone on a set s, then f induces an order isomorphism between s and its image f '' s, with the bijection coming from the injectivity on s.
Русский
Если f строго монотонна на множестве s, то она задаёт изоморфизм порядка между s и изображением f '' s.
LaTeX
$$$s \cong_o f '' s$$$
Lean4
/-- If a function `f` is strictly monotone on a set `s`, then it defines an order isomorphism
between `s` and its image. -/
protected noncomputable def orderIso {α β} [LinearOrder α] [Preorder β] (f : α → β) (s : Set α)
(hf : StrictMonoOn f s) : s ≃o f '' s
where
toEquiv := hf.injOn.bijOn_image.equiv _
map_rel_iff' := hf.le_iff_le (Subtype.property _) (Subtype.property _)
