nhdsLE_basis — Mathlib

English

On a space with a linear order and order topology, a neighborhood basis for 𝓝≤a can be taken from Ioc intervals.

Русский

Для 𝓝≤a в линейно упорядоченном пространстве с ордерной топологией базис окрестностей можно взять из интервалов Ioc.

LaTeX

$$$\\mathcal{N}_{\\le a} \\text{ has basis } \\{Ioc(l,a) : l

Lean4

theorem nhdsLE_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) :
    (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a :=
  nhdsLE_basis_of_exists_lt (exists_lt a)

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