English
Let f be strictly monotone between linear orders with order topology, and range f is order-connected. Then the topology induced by f equals the order topology on the domain.
Русский
Пусть f — строго монотонна между линейными порядками с топологией порядка, и образ диапазона f связан по порядку. Тогда индуцированная топология по f совпадает с ордерной топологией домена.
LaTeX
$$$\\text{StrictMono}(f) \\Rightarrow (\\mathrm{range}(f)).\\mathrm{OrdConnected} \\Rightarrow \\mathrm{induced}(f) = \\text{Preorder.topology}(α).$$$
Lean4
/-- The topology induced by a strictly monotone function with order-connected range is the preorder
topology. -/
nonrec theorem induced_topology_eq_preorder {α β : Type*} [LinearOrder α] [LinearOrder β] [t : TopologicalSpace β]
[OrderTopology β] {f : α → β} (hf : StrictMono f) (hc : OrdConnected (range f)) :
t.induced f = Preorder.topology α :=
by
refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_
· rcases hc.out (mem_range_self _) (mem_range_self _) ⟨not_lt.1 h₂, h₁.le⟩ with ⟨y, rfl⟩
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩
· rcases hc.out (mem_range_self _) (mem_range_self _) ⟨h₁.le, not_lt.1 h₂⟩ with ⟨y, rfl⟩
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩
