English
A strictly monotone function between linear orders with order topology is a topological embedding if its range is order-connected.
Русский
Строго монотонное отображение между линейными порядками с порядковой топологией является топологическим вложением, если образ диапазона соединён по порядку.
LaTeX
$$$f:\\alpha\\hookrightarrow\\beta\\text{ is a Topology.IsEmbedding}$, given StrictMono f and OrdConnected(range f).$$
Lean4
/-- A strictly monotone function between linear orders with order topology is a topological
embedding provided that the range of `f` is order-connected. -/
theorem isEmbedding_of_ordConnected {α β : Type*} [LinearOrder α] [LinearOrder β] [TopologicalSpace α]
[h : OrderTopology α] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : StrictMono f)
(hc : OrdConnected (range f)) : IsEmbedding f :=
⟨⟨h.1.trans <| Eq.symm <| hf.induced_topology_eq_preorder hc⟩, hf.injective⟩
