English
The following statements about neighborhoods to the right of a are equivalent: (i) s ∈ 𝓝[>] a; (ii) s ∈ 𝓝[Ioc a b] a; (iii) s ∈ 𝓝[Ioo a b] a; (iv) ∃ u ∈ Ioc a b, Ioo a u ⊆ s; (v) ∃ u ∈ Ioi a, Ioo a u ⊆ s.
Русский
Следующие условия касательно окрестностей справа от a эквивалентны: (i) s ∈ 𝓝[>] a; (ii) s ∈ 𝓝[Ioc a b] a; (iii) s ∈ 𝓝[Ioo a b] a; (iv) ∃ u ∈ Ioc a b, Ioo a u ⊆ s; (v) ∃ u ∈ Ioi a, Ioo a u ⊆ s.
LaTeX
$$$\text{TFAE}\left[ s \in \mathcal{N}_{>a},\ s \in \mathcal{N}_{Ioc(a,b)}(a),\ s \in \mathcal{N}_{Ioo(a,b)}(a),\ \exists u\in Ioc(a,b), Ioo(a,u)\subseteq s,\ \exists u\in Ioi(a), Ioo(a,u)\subseteq s \right]$$$
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_nhdsGT {a b : α} (hab : a < b) (s : Set α) :
TFAE [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s] :=
by
tfae_have 1 ↔ 2 := by rw [nhdsWithin_Ioc_eq_nhdsGT hab]
tfae_have 1 ↔ 3 := by rw [nhdsWithin_Ioo_eq_nhdsGT hab]
tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
tfae_have 5 → 1
| ⟨u, hau, hu⟩ => mem_of_superset (Ioo_mem_nhdsGT hau) hu
tfae_have 1 → 4
| h => by
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩
rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩
exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩
tfae_finish
