of_le

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

← MathLib Explorer

English

If μ is AEDisjoint on s,t and ν ≤ μ, then ν is AEDisjoint on s,t.

Русский

Если μ AEDisjoint на s,t и ν ≤ μ, то ν AEDisjoint на s,t.

LaTeX

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

Lean4

protected theorem of_le (h : AEDisjoint μ s t) {ν : Measure α} (h' : ν ≤ μ) : AEDisjoint ν s t :=
  h.of_absolutelyContinuous (Measure.absolutelyContinuous_of_le h')

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

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

Разделы

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

Аффилиация

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