arctan

Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan

URI: https://scilib.ai/kg/mathlib#Measurable.arctan

English

If exp(t f) is measurable for t ≠ 0, then f is measurable.

Русский

Если exp(t f) измерима при t ≠ 0, тогда f измерим.

LaTeX

$$$$\\forall t\\neq 0:\\; \\text{Measurable}(x \\mapsto e^{t f(x)}) \\Rightarrow \\text{Measurable}(f).$$$$

Lean4

@[measurability, fun_prop]
theorem arctan (hf : Measurable f) : Measurable fun x => arctan (f x) :=
  measurable_arctan.comp hf

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

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

Разделы

Аффилиация

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