English
There is a basis of neighborhoods for Iic a generated by Iio intervals, indexed by points greater than a.
Русский
Существует база окрестностей для Iic a, порождаемая интервалами Iio, индексируемыми точками больше a.
LaTeX
$$$(a)\ [h:\text{Nonempty }(Ioi\ a)] : HasBasis(𝓝ˢ(Iic\ a))\ (a<\cdot)\ Iio$$$
Lean4
theorem hasBasis_nhdsSet_Iic_Iio (a : α) [h : Nonempty (Ioi a)] : HasBasis (𝓝ˢ (Iic a)) (a < ·) Iio :=
by
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨b, hab, hb⟩ ↦ mem_of_superset (Iio_mem_nhdsSet_Iic hab) hb⟩⟩
rw [nhdsSet_Iic, mem_sup, mem_principal] at hs
rcases exists_Ico_subset_of_mem_nhds hs.1 (Set.nonempty_coe_sort.1 h) with ⟨b, hab, hbs⟩
exact ⟨b, hab, Iio_subset_Iio_union_Ico.trans (union_subset hs.2 hbs)⟩
