nhds_order_unbounded — Mathlib

English

If a has both a larger element and a smaller element, then nhds a can be expressed as an intersection of principal filters of Ioi and Iio across all l<a<u.

Русский

Если у a есть и большая и меньшая границы, окрестности a можно записать как пересечение нормативных фильтров через Ioi и Iio во всех l<a<u.

LaTeX

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

Lean4

theorem nhds_order_unbounded [OrderTopology α] {a : α} (hu : ∃ u, a < u) (hl : ∃ l, l < a) :
    𝓝 a = ⨅ (l) (_ : l < a) (u) (_ : a < u), 𝓟 (Ioo l u) := by
  simp only [nhds_eq_order, ← inf_biInf, ← biInf_inf, *, ← inf_principal, ← Ioi_inter_Iio]; rfl

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