nhds_bot_basis — Mathlib

English

The bottom neighborhood basis uses Iio a as basic neighborhoods around ⊥.

Русский

Базис окрестностей снизу строится из множеств Iio a.

LaTeX

$$$\\text{nhds}_{\\bot}\\;\\text{basis} = \\{ Iio(a) : a\\in\\mathbb{R} \\}$$$

Lean4

theorem nhds_bot_basis : (𝓝 (⊥ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Iio ·) :=
  by
  refine (_root_.nhds_bot_basis (α := EReal)).to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
  rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
  exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩

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