rfl

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

English

If μ1 ≪ ν and μ2 ≪ ν, then μ1 + μ2 ≪ ν.

Русский

Если μ1 ≪ ν и μ2 ≪ ν, то μ1 + μ2 ≪ ν.

LaTeX

$$$\mu_1 \ll \nu \rightarrow \mu_2 \ll \nu \rightarrow (\mu_1 + \mu_2) \ll \nu$$$

Lean4

protected theorem rfl : μ ≪ μ := fun _s hs => hs

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

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

Разделы

Аффилиация

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