English
Dual formulation: if s ⊆ Ioi(a) and s is dense towards a from above, then pulling back along the right inclusion gives the bottom filter; i.e., no nontrivial leftwards approach from above inside s.
Русский
Двойственная формулировка: если s ⊆ Ioi(a) и s плотно аппроксимирует a сверху, то обратное отображение даёт нижний фильтр; т.е. нет ненулевой аппроксимации справа от a внутри s.
LaTeX
$$$\\mathrm{comap}(\\mathrm{Subtype.val}, \\mathcal{N}_{>}(a)) = \\mathrm{atBot}$$$
Lean4
theorem comap_coe_nhdsGT_of_Ioo_subset (ha : s ⊆ Ioi a) (hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s) :
comap ((↑) : s → α) (𝓝[>] a) = atBot :=
by
apply comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha)
simp only [OrderDual.exists, Ioo_toDual]
exact hs