coe_range_mem_nhds — Mathlib

English

The image of the coercion map from ℝ≥0 to ℝ≥0∞ is a neighborhood of every finite ENNReal number r; i.e., range(↑) ∈ nhds(r).

Русский

Образ отображения включения ℝ≥0 в ℝ≥0∞ является окрестностью каждого конечного числа r; то есть range(↑) ∈ nhds(r).

LaTeX

$$$\\operatorname{range}(\\uparrow) \\in \\mathcal{N}(r)\\;\\text{for } r \\in \\mathbb{R}_{\\ge 0}$$$$

Lean4

theorem coe_range_mem_nhds : range ((↑) : ℝ≥0 → ℝ≥0∞) ∈ 𝓝 (r : ℝ≥0∞) :=
  IsOpen.mem_nhds isOpenEmbedding_coe.isOpen_range <| mem_range_self _

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