English
If f: α → β is strictly order-preserving and the auxiliary conditions H1, H2 hold, then the induced topology on α is an OrderTopology
Русский
Если f: α → β строго сохраняет порядок и выполняются дополнительные условия H1, H2, то индуцированная топология на α является OrderTopology.
LaTeX
$$$@OrderTopology _ (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₁ : ∀ {a x}, x < f a → ∃ b < a, x ≤ f b)
(H₂ : ∀ {a x}, f a < x → ∃ b > a, f b ≤ x) : @OrderTopology _ (induced f ta) _ :=
let _ := induced f ta
⟨induced_topology_eq_preorder hf (fun h _ => H₁ h) (fun h _ => H₂ h)⟩
