mono_ac

Mathlib.MeasureTheory.Integral.IntegralEqImproper

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AECover.mono_ac

English

If f is continuous on a compact set s, then f is AEStronglyMeasurable w.r.t. μ.restrict s.

Русский

Если f непрерывна на компактном множестве s, то она AEStronglyMeasurable относительно μ|_s.

LaTeX

$$$\\text{AEStronglyMeasurable } f (\\mu \\restriction s)$$$

Lean4

theorem mono_ac {ν : Measure α} {φ : ι → Set α} (hφ : AECover μ l φ) (hle : ν ≪ μ) : AECover ν l φ :=
  ⟨hle hφ.1, hφ.2⟩

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

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

Разделы

Аффилиация

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