continuous_coe

Mathlib.Topology.UniformSpace.Real

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

English

The canonical inclusion map from NNReal to ℝ, given by the coercion, is continuous.

Русский

Естественное включение NNReal в ℝ — непрерывно.

LaTeX

$$$\\text{continuous}(\\text{coe})$$$

Lean4

@[fun_prop]
theorem continuous_coe : Continuous ((↑) : ℝ≥0 → ℝ) :=
  continuous_subtype_val

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

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

Разделы

Аффилиация

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