hasBasis_nhdsSet_Iic_Iic — Mathlib

English

There is a basis for nhdsSet(Iic a) using Iic notions with a left-right order basis.

Русский

Существующая база nhdsSet(Iic a) через Iic с базисами слева и справа.

LaTeX

$$$(a)\ HasBasis(𝓝ˢ(Iic\ a)) (a<\cdot) Iic$$$

Lean4

theorem hasBasis_nhdsSet_Iic_Iic (a : α) [NeBot (𝓝[>] a)] : HasBasis (𝓝ˢ (Iic a)) (a < ·) Iic :=
  by
  have : Nonempty (Ioi a) := (Filter.nonempty_of_mem (self_mem_nhdsWithin : Ioi a ∈ 𝓝[>] a)).to_subtype
  refine (hasBasis_nhdsSet_Iic_Iio _).to_hasBasis (fun c hc ↦ ?_) (fun _ h ↦ ⟨_, h, Iio_subset_Iic_self⟩)
  simpa only [Iic_subset_Iio] using Filter.nonempty_of_mem (Ioo_mem_nhdsGT hc)

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