nhdsLE_eq_iInf_principal — Mathlib

English

For the ≤ side, the neighborhood filter below a equals the infimum over elements less than a of principal filters of left-closed intervals.

Русский

Для нижней части ≤ окрестности от a равны инфимума по элементам меньше a их простые фильтры левых интервалов.

LaTeX

$$$\\mathcal{N}_{\\le a} = \\bigwedge_{l

Lean4

theorem nhdsLE_eq_iInf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ l, l < a) :
    𝓝[≤] a = ⨅ l < a, 𝓟 (Ioc l a) := by
  simp only [nhdsLE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Ioi_inter_Iic]

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