English
In a linearly ordered space with order topology, one can equip it with an order-closed topology, i.e., the relation ≤ is closed in the product space, so that the set {(x,y) : x ≤ y} is closed in α×α.
Русский
В линейно упорядоченном пространстве с порядковой топологией можно оформить топологию как Order Closed, то есть множество {(x,y) : x ≤ y} закрыто в произведении α×α.
LaTeX
$$$\\text{In a linearly ordered space }(α,≤)\\text{ with order topology }\\{(x,y)\\in α×α : x≤y\\}\\text{ is closed in }α×α.$$$
Lean4
instance (priority := 100) to_orderClosedTopology [OrderTopology α] : OrderClosedTopology α where
isClosed_le' :=
isOpen_compl_iff.1 <|
isOpen_prod_iff.mpr fun a₁ a₂ (h : ¬a₁ ≤ a₂) =>
have h : a₂ < a₁ := lt_of_not_ge h
let ⟨u, v, hu, hv, ha₁, ha₂, h⟩ := order_separated h
⟨v, u, hv, hu, ha₂, ha₁, fun ⟨b₁, b₂⟩ ⟨h₁, h₂⟩ => not_le_of_gt <| h b₂ h₂ b₁ h₁⟩
