English
If there exists for every x < y an a with x < f(a) < y, then the order topology on α agrees with the topology induced by f.
Русский
Если для любых x < y существует a с x < f(a) < y, то ордерная топология на α совпадает с индуцированной топологией через f.
LaTeX
$$$\\text{OrderTopology}(α) = \\text{induced}(f; ta)$.$$
Lean4
theorem induced_orderTopology {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] [Preorder β]
[OrderTopology β] (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y) (H : ∀ {x y}, x < y → ∃ a, x < f a ∧ f a < y) :
@OrderTopology _ (induced f ta) _ :=
induced_orderTopology' f (hf)
(fun xa =>
let ⟨b, xb, ba⟩ := H xa;
⟨b, hf.1 ba, le_of_lt xb⟩)
fun ax =>
let ⟨b, ab, bx⟩ := H ax;
⟨b, hf.1 ab, le_of_lt bx⟩
