comap_coe_Ioi_nhdsGT — Mathlib

English

Dual formulation via dual order: comap along the left-interval map also yields the top filter under analogous hypotheses.

Русский

Двойственная формулировка аналогична: сопоставление через левый интервал даёт верхний фильтр.

LaTeX

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

Lean4

theorem comap_coe_Ioi_nhdsGT (a : α) : comap ((↑) : Ioi a → α) (𝓝[>] a) = atBot :=
  comap_coe_nhdsGT_of_Ioo_subset (Subset.refl _) fun ⟨x, hx⟩ => ⟨x, hx, Ioo_subset_Ioi_self⟩

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