trans

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.AbsolutelyContinuous.trans

English

If μ1 ≪ μ2 and μ2 ≪ μ3, then μ1 ≪ μ3 (transitivity of absolute continuity).

Русский

Если μ1 ≪ μ2 и μ2 ≪ μ3, то μ1 ≪ μ3 (порядок абсолютной непрерывности).

LaTeX

$$$\mu_1 \ll \mu_2 \rightarrow \mu_2 \ll \mu_3 \rightarrow \mu_1 \ll \mu_3$$$

Lean4

@[trans]
protected theorem trans (h1 : μ₁ ≪ μ₂) (h2 : μ₂ ≪ μ₃) : μ₁ ≪ μ₃ := fun _s hs => h1 <| h2 hs

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

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

Разделы

Аффилиация

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