nhds_eq_order — Mathlib

English

The neighborhood filter at a is the infimum of principal filters of half-intervals Ioi and Iio around a.

Русский

Окрестность точки a задаётся как наименьшая верхняя граница через множества Ioi и Iio вокруг a.

LaTeX

$$$\\mathcal{N}(a) = \\inf_{la} \\mathcal{P}(Iio(u))$$$

Lean4

theorem nhds_eq_order [OrderTopology α] (a : α) : 𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) :=
  by
  rw [OrderTopology.topology_eq_generate_intervals (α := α), nhds_generateFrom]
  simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and, iInf_exists, iInf_inf_eq,
    iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]

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