mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset

English

For a < u', a set s belongs to the right neighborhood 𝓝[>] a if and only if there exists u with a < u ≤ u' and Ioo a u ⊆ s.

Русский

Для а < u' множество s принадлежит к правой окрестности 𝓝[>] a тогда и только тогда, когда существует u > a с a < u ≤ u' и Ioo a u ⊆ s.

LaTeX

$$$\forall a,u'\,(a < u')\rightarrow (s \in 𝓝[>] a \iff \exists u\, (u \in Ioc(a,u')) , Ioo(a,u) \subseteq s)$$$

Lean4

theorem mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioc a u', Ioo a u ⊆ s :=
  (TFAE_mem_nhdsGT hu' s).out 0 3

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