English
Let X be a linearly ordered space with OrderTopology. If hd: disjoint s and closure t and a ∈ s, then the complement of ordConnectedSection(ordSeparatingSet s t) lies in nhdsWithin a of Iic a.
Русский
Пусть X — линейно упорядоченное пространство с OrderTopology. При hd: disjoint s и closure t и a ∈ s, комплемент ordConnectedSection(ordSeparatingSet s t) принадлежит nhdsWithin a на отрезке (-∞, a].
LaTeX
$$$(\operatorname{ordConnectedSection}(\operatorname{ordSeparatingSet}(s,t)))^{c} \in \nhdsWithin(a, (-\infty, a]).$$$
Lean4
theorem compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE (hd : Disjoint s (closure t)) (ha : a ∈ s) :
(ordConnectedSection <| ordSeparatingSet s t)ᶜ ∈ 𝓝[≤] a :=
by
have hd' : Disjoint (ofDual ⁻¹' s) (closure <| ofDual ⁻¹' t) := hd
have ha' : toDual a ∈ ofDual ⁻¹' s := ha
simpa only [dual_ordSeparatingSet, dual_ordConnectedSection] using
compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd' ha'
