of_absolutelyContinuous

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEDisjoint.of_absolutelyContinuous

English

If μ is AEDisjoint on s,t and ν ≪ μ, then ν is AEDisjoint on s,t as well.

Русский

Если μ и s,t образуют AEDисjoint и ν ≪ μ, то ν также AEDисjoint на s,t.

LaTeX

$$AEDisjoint(μ,s,t) ∧ ν ≪ μ → AEDisjoint(ν,s,t)$$

Lean4

protected theorem of_absolutelyContinuous (h : AEDisjoint μ s t) {ν : Measure α} (h' : ν ≪ μ) : AEDisjoint ν s t :=
  h' h

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

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

Разделы

Аффилиация

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