English
If s ⊆ Iio(b) and s is nonempty in the right way, the map from s to α sends the top filter to the interval-neighborhood at b.
Русский
Если s ⊆ Iio(b) и она удовлетворяет условиям, отображение из s в α отправляет верхний фильтр в окрестности b внутри Iio(b).
LaTeX
$$$\\mathrm{map}((\\uparrow): s \\to \\alpha)\\,(\\mathrm{atTop}) = \\mathcal{N}_{<}(b)$$$
Lean4
theorem map_coe_atTop_of_Ioo_subset (hb : s ⊆ Iio b) (hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s) :
map ((↑) : s → α) atTop = 𝓝[<] b :=
by
rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)
· have : IsEmpty s := ⟨fun x => hb'.subset (hb x.2)⟩
rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
· rw [← comap_coe_nhdsLT_of_Ioo_subset hb fun _ => hs a ha, map_comap_of_mem]
rw [Subtype.range_val]
exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)
