continuous_klFun

Mathlib.InformationTheory.KullbackLeibler.KLFun

URI: https://scilib.ai/kg/mathlib#InformationTheory.continuous_klFun

English

The function klFun is continuous on the real line.

Русский

Функция klFun непрерывна на всей прямой.

LaTeX

$$$\\mathrm{klFun} \\in C(\\mathbb{R})$$$

Lean4

/-- `klFun` is continuous. -/
@[continuity, fun_prop]
theorem continuous_klFun : Continuous klFun := by unfold klFun; fun_prop

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

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

Разделы

Аффилиация

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