nhds_top_basis — Mathlib

English

The neighborhood filter at ⊤ has a basis given by the sets Ioi a (a ∈ ℝ).

Русский

Фильтр окрестностей в ⊤ имеет базис из множест Ioi a (a ∈ ℝ).

LaTeX

$$$(\\nhds(\\top)).HasBasis(\\lambda _ : \\mathbb{R}, True) (Ioi \\cdot)$$$

Lean4

nonrec theorem nhds_top_basis : (𝓝 (⊤ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Ioi ·) :=
  by
  refine (nhds_top_basis (α := EReal)).to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩
  rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩
  exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩

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