English
If s ⊆ Iio(b) and s is nonempty and dense in the Iio(b) sense, then pulling back the left-neighborhoods at b along the inclusion recovers the top filter; i.e., the left neighbourhoods are cofinal with the ambient order from below.
Русский
Если s ⊆ Iio(b) непусто и плотно в смысле Iio, то обратное отображение левых окрестностей в b даёт верхний фильтр; левая окрестность совпадает с верхним фильтром.
LaTeX
$$$\\mathrm{comap}(\\mathrm{Subtype.val}, \\mathcal{N}_{<}(b)) = \\mathrm{atTop}$$$
Lean4
theorem comap_coe_nhdsLT_of_Ioo_subset (hb : s ⊆ Iio b) (hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s) :
comap ((↑) : s → α) (𝓝[<] b) = atTop := by
nontriviality
haveI : Nonempty s := nontrivial_iff_nonempty.1 ‹_›
rcases hs (nonempty_subtype.1 ‹_›) with ⟨a, h, hs⟩
ext u; constructor
· rintro ⟨t, ht, hts⟩
obtain ⟨x, ⟨hxa : a ≤ x, hxb : x < b⟩, hxt : Ioo x b ⊆ t⟩ := (mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset h).mp ht
obtain ⟨y, hxy, hyb⟩ := exists_between hxb
refine mem_of_superset (mem_atTop ⟨y, hs ⟨hxa.trans_lt hxy, hyb⟩⟩) ?_
rintro ⟨z, hzs⟩ (hyz : y ≤ z)
exact hts (hxt ⟨hxy.trans_le hyz, hb hzs⟩)
· intro hu
obtain ⟨x : s, hx : ∀ z, x ≤ z → z ∈ u⟩ := mem_atTop_sets.1 hu
exact ⟨Ioo x b, Ioo_mem_nhdsLT (hb x.2), fun z hz => hx _ hz.1.le⟩
