exists_Ico_subset_of_mem_nhds — Mathlib

English

In an OrderTopology α, given a neighborhood s of a and a choice with a < u for some u, there exists u with a < u and Ico(a,u) ⊆ s.

Русский

В OrderTopology α, если s — окрестность a и существует u > a, то найдется u с a < u и Ico(a,u) ⊆ s.

LaTeX

$$$\\exists u,\\ a

Lean4

theorem exists_Ico_subset_of_mem_nhds [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) (h : ∃ u, a < u) :
    ∃ u, a < u ∧ Ico a u ⊆ s :=
  let ⟨_l', hl'⟩ := h
  let ⟨l, hl⟩ := exists_Ico_subset_of_mem_nhds' hs hl'
  ⟨l, hl.1.1, hl.2⟩

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