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 the interval [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, [a,\infty)).$$$
Lean4
theorem compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE (hd : Disjoint s (closure t)) (ha : a ∈ s) :
(ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[≥] a :=
by
have hmem : tᶜ ∈ 𝓝[≥] a := by
refine mem_nhdsWithin_of_mem_nhds ?_
rw [← mem_interior_iff_mem_nhds, interior_compl]
exact disjoint_left.1 hd ha
rcases exists_Icc_mem_subset_of_mem_nhdsGE hmem with ⟨b, hab, hmem', hsub⟩
by_cases H : Disjoint (Icc a b) (ordConnectedSection <| ordSeparatingSet s t)
· exact mem_of_superset hmem' (disjoint_left.1 H)
· simp only [Set.disjoint_left, not_forall, Classical.not_not] at H
rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩
have hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a := subset_ordConnectedComponent (left_mem_Icc.2 hab) hsub
have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset
replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <| disjoint_left.1 hd ha
filter_upwards [Ico_mem_nhdsGE hac] with x hx hx'
refine hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc ?_)
refine subset_inter (subset_iUnion₂_of_subset a ha ?_) ?_
· exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩) (hsub' ⟨hac.le, hcb⟩)
· rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩
refine subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy ?_)
refine subset_ordConnectedComponent left_mem_uIcc hxy ?_
suffices c < y by
rw [uIcc_of_ge (hx.2.trans this).le]
exact ⟨hx.2.le, this.le⟩
refine lt_of_not_ge fun hyc => ?_
have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha
