mem_nhdsGT_iff_exists_Ioo_subset — Mathlib

English

For a < u', s ∈ 𝓝[>] a if and only if there exists u in Ioi a such that Ioo a u ⊆ s.

Русский

При a < u', s ∈ 𝓝[>] a тогда и только тогда, когда существует u > a such that Ioo a u ⊆ s.

LaTeX

$$$\forall a,u'\,(a < u')\Rightarrow (s \in 𝓝[>] a \iff \exists u \in Ioi a, 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`. -/
theorem mem_nhdsGT_iff_exists_Ioo_subset [NoMaxOrder α] {a : α} {s : Set α} : s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s :=
  let ⟨_u', hu'⟩ := exists_gt a
  mem_nhdsGT_iff_exists_Ioo_subset' hu'

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