isEmbedding_coe_ennreal

Mathlib.Topology.Instances.EReal.Lemmas

URI: https://scilib.ai/kg/mathlib#EReal.isEmbedding_coe_ennreal

← MathLib Explorer

English

The inclusion ℝ≥0∞ → EReal is an embedding.

Русский

Включение ℝ≥0∞ в EReal является вложением.

LaTeX

$$$\\text{IsEmbedding}((\\uparrow):\\mathbb{R}_{\ge 0}^{\\infty}\\to \\mathrm{EReal})$$$

Lean4

theorem isEmbedding_coe_ennreal : IsEmbedding ((↑) : ℝ≥0∞ → EReal) :=
  coe_ennreal_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe_ennreal]; exact ordConnected_Ici

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

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

Разделы

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

Аффилиация

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