binEntropy_continuous — Mathlib

English

The function binEntropy is continuous at every real p.

Русский

Функция binEntropy непрерывна на всей области определения; т. е. непрерывна на всей действительной числовой линии.

LaTeX

$$$\mathrm{binEntropy}$ is continuous on $\mathbb{R}$.$$

Lean4

/-- Binary entropy is continuous everywhere.
This is due to definition of `Real.log` for negative numbers. -/
@[fun_prop]
theorem binEntropy_continuous : Continuous binEntropy := by rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub'];
  fun_prop

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