mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset

English

A variant of the previous characterization using a dual order formulation.

Русский

Вариант характеристики через двойной порядок.

LaTeX

$$$s \in \mathcal{N}_{[\ge]}(a) \iff \exists u \in Ioc(a, a) \text{ with subset } (Ioc(a,u) ⊆ s)$$$

Lean4

theorem mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioc a u', Ico a u ⊆ s :=
  (TFAE_mem_nhdsGE hu' s).out 0 3 (by simp) (by simp)

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