English
Equivalence of several neighborhood conditions on the right side of a: from nhds within ≥ a to existence of l producing left-intervals.
Русский
Эквивалентность условий окрестностей справа от точки: от nhdsWithin до существования l, задающего интервалы слева.
LaTeX
$$$\mathrm{TFAE}\!\left[ s \in \mathcal{N}_{[\ge]}(a), \ s \in \mathcal{N}_{[a,b]}(a), \ s \in \mathcal{N}_{[a,b)}(a), \ \exists l \in Ioc(a,b), Ico(a,u) \subseteq s, \ \exists l \in Ioi(a), Ico(a,u) \subseteq s \right]$$
Lean4
/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`, provided `a` is not a bottom element. -/
theorem mem_nhdsLT_iff_exists_Ioo_subset' {a l' : α} {s : Set α} (hl' : l' < a) :
s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s :=
(TFAE_mem_nhdsLT hl' s).out 0 4
