map_coe_Ioi_atBot — Mathlib

English

The coe map for Ioi atBot is the left-infinite open interval neighbourhood at the bottom endpoint in the dual order.

Русский

Коэф-представление Ioi внизу соответствует левой окрестности снизу в двойственном порядке.

LaTeX

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

Lean4

@[simp]
theorem map_coe_Ioi_atBot (a : α) : map ((↑) : Ioi a → α) atBot = 𝓝[>] a :=
  map_coe_atBot_of_Ioo_subset (Subset.refl _) fun b hb => ⟨b, hb, Ioo_subset_Ioi_self⟩

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