hasMeasurablePow — Mathlib

English

The real numbers admit a MeasurablePow structure, i.e., the power operation on reals is measurable.

Русский

У действительных чисел есть структура измеримого возведения в степень; операция возведения в степень измерима.

LaTeX

$$$\\text{Real.HasMeasurablePow}$$$

Lean4

instance hasMeasurablePow : MeasurablePow ℝ ℝ :=
  ⟨Complex.measurable_re.comp <|
      (Complex.measurable_ofReal.comp measurable_fst).pow (Complex.measurable_ofReal.comp measurable_snd)⟩

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