carg

Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

URI: https://scilib.ai/kg/mathlib#AEMeasurable.carg

English

Let f be almost everywhere measurable; then x ↦ arg(f(x)) is almost everywhere measurable.

Русский

Пусть f ~почти всюду измерима; тогда x ↦ arg(f(x)) ~почти всюду измерима.

LaTeX

$$$AEMeasurable\\ f\\ μ \\rightarrow AEMeasurable\\bigl(\\lambda x. \\arg(f(x))\\bigr)\\ μ$$$

Lean4

@[measurability, fun_prop]
protected theorem carg : AEMeasurable (fun x ↦ arg (f x)) μ :=
  measurable_arg.comp_aemeasurable hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru