nhdsGE_basis_of_exists_gt — Mathlib

English

If there exists a point strictly above a, then a basis for 𝓝≥a is given by sets Ico(a,u) with u > a.

Русский

Если существует точка выше a, тогда базис окрестностей 𝓝≥a задаётся через интервалы Ico(a,u) с u>a.

LaTeX

$$$(\\mathcal{N}_{\\ge a}) \\text{ has basis } \\{I_{>a}(a,u) : u>a\\}.$$$

Lean4

theorem nhdsGE_basis_of_exists_gt [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ u, a < u) :
    (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u :=
  (nhdsGE_eq_iInf_principal ha).symm ▸
    hasBasis_biInf_principal
      (fun b hb c hc =>
        ⟨min b c, lt_min hb hc, Ico_subset_Ico_right (min_le_left _ _), Ico_subset_Ico_right (min_le_right _ _)⟩)
      ha

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