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)