nhds_coe_coe — Mathlib

English

The neighborhood of a pair of finite reals in EReal corresponds to the pushforward of the product neighborhood in ℝ×ℝ under the coordinatewise inclusion.

Русский

Окрестности пары конечных чисел в EReal соответствуют образу произведения окрестностей в ℝ×ℝ через попарное включение.

LaTeX

$$$\\mathcal{N}((r:\\mathrm{EReal}, p:\\mathrm{EReal})) = (\\mathcal{N}(r,p)).map (fun q : \\mathbb{R}\\times\\mathbb{R} \\Rightarrow (q.1:\\mathrm{EReal}, q.2:\\mathrm{EReal}))$$$

Lean4

theorem nhds_coe_coe {r p : ℝ} : 𝓝 ((r : EReal), (p : EReal)) = (𝓝 (r, p)).map fun p : ℝ × ℝ => (↑p.1, ↑p.2) :=
  ((isOpenEmbedding_coe.prodMap isOpenEmbedding_coe).map_nhds_eq (r, p)).symm

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