nhds_coe_coe — Mathlib

English

The neighborhoods at ENNReal-points are the pushforward of neighborhoods from NNReal via the coe map, for pairs.

Русский

Окрестности в ENNReal-парe совпадают с изображением окрестностей NNReal через каноническое вложение.

LaTeX

$$$\mathcal{N}(((r : \mathbb{R}_{\ge 0∞}), (p : \mathbb{R}_{\ge 0∞}))) = (\mathcal{N}(r,p)).map (\lambda q: (\uparrow q.1, \uparrow q.2)).$$$

Lean4

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

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