English
Equivalence of five right-sided left- and within-interval neighborhood statements at the left end.
Русский
Эквивалентность пяти утверждений о правой стороне левой окрестности на левой границе.
LaTeX
$$$\mathrm{TFAE}\!\left[ s \in \mathcal{N}_{[\le]} a, s \in \mathcal{N}_{[\text{Icc} a b]} a, s \in \mathcal{N}_{[\text{Ico} a b]} a, \exists l \in Ico(a,b), Ioc(l,b) \subseteq s, \exists l \in Iio(b), Ioc(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_nhdsLE {a b : α} (h : a < b) (s : Set α) :
TFAE
[s ∈ 𝓝[≤] b, -- 0 : `s` is a neighborhood of `b` within `(-∞, b]`
s ∈ 𝓝[Icc a b] b, -- 1 : `s` is a neighborhood of `b` within `[a, b]`
s ∈ 𝓝[Ioc a b] b, -- 2 : `s` is a neighborhood of `b` within `(a, b]`
∃ l ∈ Ico a b, Ioc l b ⊆ s, -- 3 : `s` includes `(l, b]` for some `l ∈ [a, b)`
∃ l ∈ Iio b, Ioc l b ⊆ s] :=
by -- 4 : `s` includes `(l, b]` for some `l < b`
simpa using TFAE_mem_nhdsGE h.dual (ofDual ⁻¹' s)
