measure_smul_null

Mathlib.MeasureTheory.Group.Action

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_smul_null

English

If s has zero μ-measure, then its image under any smul by c also has zero μ-measure.

Русский

Если множество s имеет нулевую меру μ, то и его образ под действием c тоже имеет нулевую меру.

LaTeX

$$$\\mu(s)=0 \\Rightarrow \\mu(c\\cdot s)=0$$$

Lean4

@[to_additive]
theorem measure_smul_null {s} (h : μ s = 0) (c : G) : μ (c • s) = 0 :=
  (measure_smul_eq_zero_iff _).2 h

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

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

Разделы

Аффилиация

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