English
A set s is a neighborhood of a in [a, ∞) iff there exists u ∈ (a, ∞) such that Ioc(a,u) ⊆ s.
Русский
Окрестность s в [a, ∞) равна, если есть u ∈ (a, ∞), такой что Ioc(a,u) ⊆ s.
LaTeX
$$$s \in \mathcal{N}_{[\ge]}(a) \iff \exists u \in Ioc(a, u), Ioc(a,u) \subseteq s$$
Lean4
/-- The following statements are equivalent:
0. `s` is a neighborhood of `a` within `[a, +∞)`;
1. `s` is a neighborhood of `a` within `[a, b]`;
2. `s` is a neighborhood of `a` within `[a, b)`;
3. `s` includes `[a, u)` for some `u ∈ (a, b]`;
4. `s` includes `[a, u)` for some `u > a`.
-/
theorem TFAE_mem_nhdsGE {a b : α} (hab : a < b) (s : Set α) :
TFAE [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s] :=
by
tfae_have 1 ↔ 2 := by rw [nhdsWithin_Icc_eq_nhdsGE hab]
tfae_have 1 ↔ 3 := by rw [nhdsWithin_Ico_eq_nhdsGE hab]
tfae_have 1 ↔ 5 := (nhdsGE_basis_of_exists_gt ⟨b, hab⟩).mem_iff
tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
tfae_have 5 → 4
| ⟨u, hua, hus⟩ =>
⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩, (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩
tfae_finish
