English
Suppose f: α → β reflects the order in both directions (x < y iff f(x) < f(y)) and certain comparability conditions (H1, H2) hold. Then the topology induced by f from β coincides with the order topology on α.
Русский
Пусть отображение f: α → β отражает порядок в обе стороны и выполняются дополнительные условия H1, H2. Тогда индуцированная через f топология на α совпадает с ордной топологией α.
LaTeX
$$$\\text{Induced}(f; β) = \\text{Preorder.topology}(α).$$$
Lean4
theorem induced_topology_eq_preorder [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : α → β}
(hf : ∀ {x y}, f x < f y ↔ x < y) (H₁ : ∀ {a b x}, b < f a → ¬(b < f x) → ∃ y, y < a ∧ b ≤ f y)
(H₂ : ∀ {a b x}, f a < b → ¬(f x < b) → ∃ y, a < y ∧ f y ≤ b) :
induced f ‹TopologicalSpace β› = Preorder.topology α :=
by
let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩
refine le_antisymm (induced_topology_le_preorder hf) ?_
refine le_of_nhds_le_nhds fun a => ?_
simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal]
refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)
· rcases em (∃ x, ¬(b < f x)) with (⟨x, hx⟩ | hb)
· rcases H₁ hb hx with ⟨y, hya, hyb⟩
exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => hyb.trans_lt (hf.2 hz))
· push_neg at hb
exact le_principal_iff.2 (univ_mem' hb)
· rcases em (∃ x, ¬(f x < b)) with (⟨x, hx⟩ | hb)
· rcases H₂ hb hx with ⟨y, hya, hyb⟩
exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb)
· push_neg at hb
exact le_principal_iff.2 (univ_mem' hb)
