English
Let α and β be preordered sets, and f: α → β be order-preserving in the sense that x < y iff f(x) < f(y). Then the topology induced on α by f from β is not stronger than the order topology on α.
Русский
Пусть α, β — частично упорядоченные множества, и f: α → β сохраняет порядок так, что x < y тогда и только f(x) < f(y). Тогда топология, индукцированная через f на α из β, не сильнее (не строже) последовательной ордной топологии на α.
LaTeX
$$$\\text{Induced}(f; β) \\leq \\text{Preorder.topology}(α).$$$
Lean4
theorem induced_topology_le_preorder [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : α → β}
(hf : ∀ {x y}, f x < f y ↔ x < y) : induced f ‹TopologicalSpace β› ≤ Preorder.topology α :=
by
let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩
refine le_of_nhds_le_nhds fun x => ?_
simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal, Ioi, Iio, ← hf]
refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)
exacts [iInf₂_le (f a) ha, iInf₂_le (f a) ha]
