measure_smul_eq_zero_iff — Mathlib

English

Let f: α → β be equivariant with respect to a group M acting on α and β, and μ on α is M-invariant; if f is measurable, then the pushforward measure map f μ on β is M-invariant as well.

Русский

Пусть f: α → β совместимо (вариантно) с действием группы M на α и β, и μ на α инвариантна относительно M; если f измеримо, то образующая мера map f μ на β тоже инвариантна относительно M.

LaTeX

$$$\\text{SMulInvariantMeasure } M \\alpha \\mu \\wedge (\\forall m,a, f(m \\cdot a) = m \\cdot f(a)) \\\\ \\wedge \\text{Measurable}(f) \\Rightarrow \\text{SMulInvariantMeasure } M \\beta (\\operatorname{map} f \\mu)$$$

Lean4

@[to_additive]
theorem measure_smul_eq_zero_iff {s} (c : G) : μ (c • s) = 0 ↔ μ s = 0 := by rw [measure_smul]

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