exists_Ioc_subset_of_mem_nhds — Mathlib

English

In an ordered topological space, given a neighborhood s of a and l < a, there exists l' with l < l' ≤ a such that Ioc(l', a) ⊆ s.

Русский

В упорядоченном топологическом пространстве при s ∈ nhds(a) и l < a существует l' с l < l' ≤ a и Ioc(l', a) ⊆ s.

LaTeX

$$$\\forall a\\in α,\\forall s\\subseteq α\\, (s\\in 𝓝 a)\\ ;\\ \\forall l\\in α\\ (l

Lean4

theorem exists_Ioc_subset_of_mem_nhds [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) (h : ∃ l, l < a) :
    ∃ l < a, Ioc l a ⊆ s :=
  (nhdsLE_basis_of_exists_lt h).mem_iff.mp (nhdsWithin_le_nhds hs)

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