comap_coe_Iio_nhdsLT — Mathlib

English

The left-limit comap lemma: the comap of the left-neighborhood filter at a with Iio is the top filter in the dual order sense.

Русский

Оформление левой окрестности через Iio возвращает верхний фильтр в двойственном порядке.

LaTeX

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

Lean4

theorem comap_coe_Iio_nhdsLT (a : α) : comap ((↑) : Iio a → α) (𝓝[<] a) = atTop :=
  comap_coe_Ioi_nhdsGT (α := αᵒᵈ) a

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