continuous_ofReal

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#ENNReal.continuous_ofReal

English

The ENNReal-coe map from Real via ofReal is continuous; i.e., ENNReal.ofReal is continuous.

Русский

Отображение ENNReal.fromReal через ofReal непрерывно.

LaTeX

$$$\\operatorname{Continuous} (\\mathrm{ENNReal}.ofReal)$$$

Lean4

theorem continuous_ofReal : Continuous ENNReal.ofReal :=
  (continuous_coe_iff.2 continuous_id).comp continuous_real_toNNReal

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

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

Разделы

Аффилиация

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