isEmbedding_coe

Mathlib.Topology.Algebra.Ring.Real

URI: https://scilib.ai/kg/mathlib#ENNReal.isEmbedding_coe

← MathLib Explorer

English

The natural inclusion NNReal → ENNReal is an embedding.

Русский

Естественное вложение \mathbb{R}_{\ge 0} в ENNReal является вложением (embedding).

LaTeX

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

Lean4

theorem isEmbedding_coe : IsEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) :=
  coe_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe']; exact ordConnected_Iio

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru