English
Let a be an element with no maximum; a set s is a neighborhood of a within (a, ∞) iff there exists u > a such that (a, u] ⊆ s.
Русский
Пусть a не максимален. Тогда s является окрестностью a внутри (a, бесконечность), если и только если существует u > a такое, что (a, u] ⊆ s.
LaTeX
$$$s \in \mathcal{N}_{(>a)} \; a \iff \exists u \in I^{+}(a), (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_Ioc_subset [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s :=
by
rw [mem_nhdsGT_iff_exists_Ioo_subset]
constructor
· rintro ⟨u, au, as⟩
rcases exists_between au with ⟨v, hv⟩
exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩
· rintro ⟨u, au, as⟩
exact ⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩
