English
The pushforward of the top filter along the inclusion from s into α equals the Ioo-neighborhood at b when s ⊆ Iio b and appropriate density conditions hold.
Русский
Отображение верхнего фильтра через включение из s в α равно окрестности Ioo при b, если s ⊆ Iio(b) и выполняются плотные условия.
LaTeX
$$$\\mathrm{map}((\\uparrow): s \\to \\alpha)\\,\\mathrm{atTop} = \\mathcal{N}_{Iio(b)}(b)$$$
Lean4
/-- The `atTop` filter for an open interval `Ioo a b` comes from the left-neighbourhoods filter at
the right endpoint in the ambient order. -/
theorem comap_coe_Ioo_nhdsLT (a b : α) : comap ((↑) : Ioo a b → α) (𝓝[<] b) = atTop :=
comap_coe_nhdsLT_of_Ioo_subset Ioo_subset_Iio_self fun h => ⟨a, nonempty_Ioo.1 h, Subset.refl _⟩
