map_coe_atTop

Mathlib.Topology.Instances.NNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#NNReal.map_coe_atTop

English

The map toReal sends atTop to atTop; i.e., map toReal atTop = atTop.

Русский

Отображение toReal сохраняет фильтр atTop: map toReal atTop = atTop.

LaTeX

$$$map\\ toReal\\ atTop = atTop$$$

Lean4

@[simp]
theorem map_coe_atTop : map toReal atTop = atTop :=
  map_val_Ici_atTop 0

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

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

Разделы

Аффилиация

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