map_toNNReal_atTop

Mathlib.Topology.Instances.NNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#Real.map_toNNReal_atTop

← MathLib Explorer

English

The map Real.toNNReal commutes with atTop: map Real.toNNReal atTop = atTop.

Русский

Согласование Real.toNNReal с atTop: map Real.toNNReal atTop = atTop.

LaTeX

$$$Real.map_toNNReal_atTop = atTop$$$

Lean4

@[simp]
theorem _root_.Real.map_toNNReal_atTop : map Real.toNNReal atTop = atTop := by
  rw [← map_coe_atTop, Function.LeftInverse.filter_map @Real.toNNReal_coe]

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

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

Разделы

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

Аффилиация

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