ordConnectedComponent_mem_nhds — Mathlib

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)

Похожие утверждения