nhdsLE_basis_of_exists_lt — Mathlib

English

Under no-max-order assumption, the above-basis for 𝓝≥a can be chosen with Ico(a,u).

Русский

При отсутствии предположения о максимальном элементе можно выбрать базис Ico(a,u).

LaTeX

$$$\\mathcal{N}_{\\ge a} \\text{ has basis } \\{I_{0}(a,u) : a

Lean4

theorem nhdsLE_basis_of_exists_lt [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ l, l < a) :
    (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a :=
  by
  convert nhdsGE_basis_of_exists_gt (α := αᵒᵈ) ha using 2
  exact Ico_toDual.symm

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