nhds_coe — Mathlib

English

The neighborhood of a real number viewed in EReal matches the pushforward of the real neighborhood: 𝓝(r in EReal) = (𝓝 r).map (↑).

Русский

Окрестности числа r в EReal равны образу окрестностей r через включение: 𝓝(r) = (𝓝 r).map (↑).

LaTeX

$$$\\mathcal{N}(r\\!:\\!\\mathrm{EReal}) = (\\mathcal{N} r).\\mathrm{map}(\\uparrow)$$$

Lean4

theorem nhds_coe {r : ℝ} : 𝓝 (r : EReal) = (𝓝 r).map (↑) :=
  (isOpenEmbedding_coe.map_nhds_eq r).symm

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