comap_coe_nhdsGT_of_Ioo_subset — Mathlib

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

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