map_coe_Ioo_atBot — Mathlib

English

Another variant of mapping a left-interval to the ambient neighborhood at the right endpoint in the open interval setting.

Русский

Ещё один вариант отображения через Ioo в окрестности справа от конца интервала.

LaTeX

$$$\\mathrm{map}((\\uparrow):s\\to \\alpha)\\ infty = \\mathcal{N}_{<}(b)$$$

Lean4

@[simp]
theorem map_coe_Ioo_atBot {a b : α} (h : a < b) : map ((↑) : Ioo a b → α) atBot = 𝓝[>] a :=
  map_coe_atBot_of_Ioo_subset Ioo_subset_Ioi_self fun _ _ => ⟨_, h, Subset.refl _⟩

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