English
Equivalence of several right-neighborhood statements around a and values Ioi, Ico, Ioc, Icc in the ge-side.
Русский
Эквивалентность нескольких утверждений о правой окрестности вокруг a с использованием Ioi, Ico, Ioc, Icc.
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,l) \subseteq s, \exists l \in Ioi(a), Ico(a,l) \subseteq s]$$$
Lean4
theorem nhdsGE_basis_Ico [NoMaxOrder α] (a : α) : (𝓝[≥] a).HasBasis (fun u => a < u) (Ico a) :=
⟨fun _ => mem_nhdsGE_iff_exists_Ico_subset⟩