English
Right neighborhoods basis via closed intervals Icc a u with a < u, using no maximum element and dense order.
Русский
Базис правых окрестностей через замкнутые интервалы Icc a u с a < u при отсутствии максимального элемента и плотном порядке.
LaTeX
$$$(NoMaxOrder\ α) \; \&\; (DenselyOrdered\ α) \Rightarrow (\mathcal{N}_{[\ge]} a).HasBasis (a<·) (Icc\ a)$$$
Lean4
/-- The filter of right neighborhoods has a basis of closed intervals. -/
theorem nhdsGE_basis_Icc [NoMaxOrder α] [DenselyOrdered α] {a : α} : (𝓝[≥] a).HasBasis (a < ·) (Icc a) :=
(nhdsGE_basis _).to_hasBasis (fun _u hu ↦ (exists_between hu).imp fun _v hv ↦ hv.imp_right Icc_subset_Ico_right)
fun u hu ↦ ⟨u, hu, Ico_subset_Icc_self⟩
