mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset

English

An explicit equivalent formulation of nhds left-neighborhoods using Ico and Ioo intervals inside left side.

Русский

Уточненная эквивалентная формулировка левых окрестностей через интервалы Ico и Ioo слева.

LaTeX

$$$\mathrm{TFAE}\!\left[ s \in \mathcal{N}_{(-\infty,b)}(b),\ \exists l\in Ico(a,b), Ioo(l,b)\subseteq s,\ \dots \right]$$

Lean4

theorem mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[<] a ↔ ∃ l ∈ Ico l' a, Ioo l a ⊆ s :=
  (TFAE_mem_nhdsLT hl' s).out 0 3

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