mul_log — Mathlib

English

If f: α → ℝ is continuous, then the function a ↦ f(a) log(f(a)) is continuous.

Русский

Если f: α → ℝ непрерывна, то a ↦ f(a) log(f(a)) непрерывна.

LaTeX

$$$\text{If } f:\alpha \to \mathbb{R} \text{ is continuous, then } a \mapsto f(a) \log f(a) \text{ is continuous.}$$$

Lean4

@[fun_prop]
theorem mul_log {α : Type*} [TopologicalSpace α] {f : α → ℝ} (hf : Continuous f) : Continuous fun a ↦ f a * log (f a) :=
  continuous_mul_log.comp hf

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