English
In a linear order with order topology, for any a and s, ordConnectedComponent(s,a) ∈ 𝓝(a) iff s ∈ 𝓝(a).
Русский
В линейном порядке с порядковой топологией для любых a и s: ordConnectedComponent(s,a) ∈ 𝓝(a) тогда и только тогда, когда s ∈ 𝓝(a).
LaTeX
$$$\operatorname{ordConnectedComponent}(s,a) \in \nhds(a) \iff s \in \nhds(a).$$$
Lean4
@[simp]
theorem ordConnectedComponent_mem_nhds : ordConnectedComponent s a ∈ 𝓝 a ↔ s ∈ 𝓝 a :=
by
refine ⟨fun h => mem_of_superset h ordConnectedComponent_subset, fun h => ?_⟩
rcases exists_Icc_mem_subset_of_mem_nhds h with ⟨b, c, ha, ha', hs⟩
exact mem_of_superset ha' (subset_ordConnectedComponent ha hs)