comap_coe_Ioo_nhdsGT — Mathlib

English

For any a < b, the comap of the left-interval neighborhood at b along the inclusion from Ioo(a,b) to α is the top filter.

Русский

Для любых a < b сопоставление по включению Ioo(a,b) к α левой окрестности в b даёт верхний фильтр.

LaTeX

$$$\\mathrm{comap}((\\uparrow):Ioo(a,b)\\to \\alpha)(\\mathcal{N}_{<}(b)) = \\mathrm{atTop}$$$

Lean4

/-- The `atBot` filter for an open interval `Ioo a b` comes from the right-neighbourhoods filter at
the left endpoint in the ambient order. -/
theorem comap_coe_Ioo_nhdsGT (a b : α) : comap ((↑) : Ioo a b → α) (𝓝[>] a) = atBot :=
  comap_coe_nhdsGT_of_Ioo_subset Ioo_subset_Ioi_self fun h => ⟨b, nonempty_Ioo.1 h, Subset.refl _⟩

Похожие утверждения