mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset

English

For hl' = l' < a, s ∈ nhdsLE(a) iff there exists l ∈ Ico(l',a) with Ioc(l,a) ⊆ s.

Русский

Для hl' < a: s ∈ nhdsLE(a) эквивалентно существованию l в Ico(l',a) с Ioc(l,a) ⊆ s.

LaTeX

$$$s \in \mathcal{N}_{[\le]} a \iff \exists l \in Ico(l',a), Ioc(l,a) \subseteq s$$

Lean4

theorem mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[≤] a ↔ ∃ l ∈ Ico l' a, Ioc l a ⊆ s :=
  (TFAE_mem_nhdsLE hl' s).out 0 3 (by simp) (by simp)

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