continuous_real_toNNReal

Mathlib.Topology.Instances.NNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#continuous_real_toNNReal

English

The map x ↦ Real.toNNReal(x) from ℝ to ℝ≥0 is continuous.

Русский

Отображение x ↦ Real.toNNReal(x) из ℝ в ℝ≥0 непрерывно.

LaTeX

$$$\mathrm{Continuous}(Real.toNNReal)$$$

Lean4

@[fun_prop]
theorem _root_.continuous_real_toNNReal : Continuous Real.toNNReal :=
  (continuous_id.max continuous_const).subtype_mk _

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

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

Разделы

Аффилиация

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