ennreal_log — Mathlib

English

If f is measurable, then the composition log ∘ f is measurable.

Русский

Если f измерима, то композиция log ∘ f измерима.

LaTeX

$$$f:\alpha \to \mathbb{R}_{\ge 0}^{\infty}$ измерима\Rightarrow\ x \mapsto \log(f(x))$ измерима$$

Lean4

@[measurability, fun_prop]
theorem _root_.Measurable.ennreal_log {α : Type*} {_ : MeasurableSpace α} {f : α → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun x ↦ log (f x) :=
  measurable_log.comp hf

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