English
For a < b, the following five statements about a neighborhood of b within negative direction are equivalent: (i) s ∈ nhds[<] b, (ii) s ∈ nhds[a,b) around b, (iii) s ∈ nhds(a,b), (iv) ∃ l ∈ [a,b) with (l,b) ⊆ s, (v) ∃ l < b with (l,b) ⊆ s.
Русский
Для a < b пара равносильностей: окрестность b слева, внутри [a,b), внутри (a,b), существование l ∈ [a,b) с (l,b) ⊆ s и существование l < b с (l,b) ⊆ s эквивалентны.
LaTeX
$$$\mathrm{TFAE}\!\left[ s \in \mathcal{N}_{(-\infty,b)}(b),\ s \in \mathcal{N}_{[a,b)}(b),\ s \in \mathcal{N}_{(a,b)}(b),\ \exists l\in [a,b),\ Ioo(l,b) \subseteq s,\ \exists l< b,\ Ioo(l,b) \subseteq s \right]$$
Lean4
/-- The following statements are equivalent:
0. `s` is a neighborhood of `b` within `(-∞, b)`
1. `s` is a neighborhood of `b` within `[a, b)`
2. `s` is a neighborhood of `b` within `(a, b)`
3. `s` includes `(l, b)` for some `l ∈ [a, b)`
4. `s` includes `(l, b)` for some `l < b` -/
theorem TFAE_mem_nhdsLT {a b : α} (h : a < b) (s : Set α) :
TFAE
[s ∈ 𝓝[<] b, -- 0 : `s` is a neighborhood of `b` within `(-∞, b)`
s ∈ 𝓝[Ico a b] b, -- 1 : `s` is a neighborhood of `b` within `[a, b)`
s ∈ 𝓝[Ioo a b] b, -- 2 : `s` is a neighborhood of `b` within `(a, b)`
∃ l ∈ Ico a b, Ioo l b ⊆ s, -- 3 : `s` includes `(l, b)` for some `l ∈ [a, b)`
∃ l ∈ Iio b, Ioo l b ⊆ s] :=
by -- 4 : `s` includes `(l, b)` for some `l < b`
simpa using TFAE_mem_nhdsGT h.dual (ofDual ⁻¹' s)
