map_coe_atBot_of_Ioo_subset — Mathlib

English

Under the left-subset condition, the pushforward along inclusion from s maps the bottom filter to the Ioi-type neighborhood at a.

Русский

При условии подмножества слева карта отображения через включение отправляет нижний фильтр в окрестности справа от a.

LaTeX

$$$\\mathrm{map}((\\uparrow): s \\to \\alpha)\\,\\mathrm{atBot} = \\mathcal{N}_{>}(a)$$$

Lean4

theorem map_coe_atBot_of_Ioo_subset (ha : s ⊆ Ioi a) (hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s) :
    map ((↑) : s → α) atBot = 𝓝[>] a := by
  -- the elaborator gets stuck without `(... :)`

  refine (map_coe_atTop_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha) fun b' hb' => ?_ :)
  simpa using hs b' hb'

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