nhdsLE_basis_Icc — Mathlib

English

Left neighborhoods also have a basis consisting of closed intervals Icc l a with l < a.

Русский

Левые окрестности имеют базис из замкнутых интервалов Icc(l,a) с l < a.

LaTeX

$$$(nhdsWithin a (\mathbb{I}\!_{\le} a)).HasBasis (\lambda x. x < a) (Icc \cdot a)$$

Lean4

/-- The filter of left neighborhoods has a basis of closed intervals. -/
theorem nhdsLE_basis_Icc [NoMinOrder α] [DenselyOrdered α] {a : α} : (𝓝[≤] a).HasBasis (· < a) (Icc · a) :=
  ⟨fun _ ↦ mem_nhdsLE_iff_exists_Icc_subset⟩

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