refl

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

English

For measures μ1, μ2, ν on α, μ1 + μ2 ≪ ν iff μ1 ≪ ν and μ2 ≪ ν.

Русский

Для мер μ1, μ2, ν на α, μ1 + μ2 ≪ ν тогда и только тогда, когда μ1 ≪ ν и μ2 ≪ ν.

LaTeX

$$$\mu_1 + \mu_2 \ll \nu \iff (\mu_1 \ll \nu) \wedge (\mu_2 \ll \nu)$$$

Lean4

@[refl]
protected theorem refl {_m0 : MeasurableSpace α} (μ : Measure α) : μ ≪ μ :=
  rfl.absolutelyContinuous

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

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

Разделы

Аффилиация

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