hasMeasurablePow — Mathlib

English

The complex field carries a MeasurablePow structure, i.e., the power operation on complex numbers is measurable in its arguments.

Русский

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

LaTeX

$$$\\text{Complex.HasMeasurablePow}$$$

Lean4

instance hasMeasurablePow : MeasurablePow ℂ ℂ :=
  ⟨Measurable.ite (measurable_fst (measurableSet_singleton 0))
      (Measurable.ite (measurable_snd (measurableSet_singleton 0)) measurable_one measurable_zero)
      (measurable_fst.clog.mul measurable_snd).cexp⟩

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