mem_nhdsGT_iff_exists_Ioo_subset'

English

For no-maximum-order α, a neighborhood to the right 𝓝[>] a contains some interval Ioo a u with a < u.

Русский

Если порядок не имеет максимума, то правая окрестность 𝓝[>] a содержит некоторый интервал Ioo a u при a < u.

LaTeX

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

Lean4

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u < u'`, provided `a` is not a top element. -/
theorem mem_nhdsGT_iff_exists_Ioo_subset' {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s :=
  (TFAE_mem_nhdsGT hu' s).out 0 4

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