continuous_div_const

Mathlib.Topology.Instances.ENNReal.Lemmas

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

← MathLib Explorer

English

For ENNReal, the map x ↦ x / c is continuous when c ≠ 0.

Русский

Для ENNReal отображение x ↦ x / c непрерывно при c ≠ 0.

LaTeX

$$$\\\\forall c \\\\neq 0, \\\\text{Continuous } (\\\\lambda x, x / c).$$$

Lean4

@[fun_prop]
protected theorem continuous_div_const (c : ℝ≥0∞) (c_ne_zero : c ≠ 0) : Continuous fun x : ℝ≥0∞ => x / c :=
  ENNReal.continuous_mul_const <| ENNReal.inv_ne_top.2 c_ne_zero

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

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

Разделы

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

Аффилиация

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