instIsRefl

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

English

From AC add_left_iff, μ1 + μ2 ≪ ν iff μ1 ≪ ν and μ2 ≪ ν.

Русский

По следствию add_left_iff, μ1 + μ2 ≪ ν тогда и только тогда, когда μ1 ≪ ν и μ2 ≪ ν.

LaTeX

$$$\text{AddLeft}(\mu_1,\mu_2) \iff (\mu_1 \ll \nu) \land (\mu_2 \ll \nu)$$$

Lean4

instance instIsRefl {_ : MeasurableSpace α} : IsRefl (Measure α) (· ≪ ·) :=
  ⟨fun _ => AbsolutelyContinuous.rfl⟩

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

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

Разделы

Аффилиация

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