absolutelyContinuous_of_eq

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

English

If μ1 ≪ μ2 and μ2 ≪ μ3, then μ1 ≪ μ3.

Русский

Если μ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

theorem absolutelyContinuous_of_eq (h : μ = ν) : μ ≪ ν :=
  h.le.absolutelyContinuous

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

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

Разделы

Аффилиация

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