isClosedEmbedding_coe_ennreal

Mathlib.Topology.Instances.EReal.Lemmas

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

← MathLib Explorer

English

The inclusion ℝ≥0∞ → EReal is a closed embedding.

Русский

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

LaTeX

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

Lean4

theorem isClosedEmbedding_coe_ennreal : IsClosedEmbedding ((↑) : ℝ≥0∞ → EReal) :=
  ⟨isEmbedding_coe_ennreal, by rw [range_coe_ennreal]; exact isClosed_Ici⟩

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

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

Разделы

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

Аффилиация

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