nhdsGE_basis — Mathlib

English

A refined statement of nhds≥a basis via HasBasis with a transfer to a dual setting.

Русский

Уточнённое утверждение базиса окрестностей 𝓝≥a через HasBasis с переносом в двойственное окружение.

LaTeX

$$$\\mathcal{N}_{\\ge a} \\text{ has HasBasis etc.}$$$

Lean4

theorem nhdsGE_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) :
    (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u :=
  nhdsGE_basis_of_exists_gt (exists_gt a)

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