isOpenEmbedding_coe — Mathlib

English

The embedding NNReal → ENNReal is an open embedding; its image is open in ENNReal.

Русский

Встраивание NNReal в ENNReal является открытым вложением; образ открыт в ENNReal.

LaTeX

$$$\uparrow: \mathbb{R}_{\ge 0} \to \mathbb{R}_{\ge 0}^{\infty}$ is an open embedding.$$

Lean4

theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) :=
  ⟨isEmbedding_coe, by rw [range_coe']; exact isOpen_Iio⟩

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