inv

Mathlib.MeasureTheory.Group.Arithmetic

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

← MathLib Explorer

English

If f is almost everywhere measurable, then f^{-1} is almost everywhere measurable.

Русский

Если f измерима почти всюду, то f^{-1} измерима почти всюду.

LaTeX

$$$AEMeasurable\\ f\\ \\mu \\Rightarrow AEMeasurable\\ (fun x \\mapsto f(x)^{-1})\\ mu$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem inv (hf : AEMeasurable f μ) : AEMeasurable (fun x => (f x)⁻¹) μ :=
  measurable_inv.comp_aemeasurable hf

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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