restrict_restrict — Mathlib

English

For any t, the double restriction distributes: (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t).

Русский

Для любого t двойное ограничение распределяется так: (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t).

LaTeX

$$$(\\mu \\restrict t)\\restrict (g\\cdot s) = \\mu \\restrict (g\\cdot s \\cap t)$$$

Lean4

@[to_additive]
theorem restrict_restrict (h : IsFundamentalDomain G s μ) (g : G) (t : Set α) :
    (μ.restrict t).restrict (g • s) = μ.restrict (g • s ∩ t) :=
  restrict_restrict₀ ((h.nullMeasurableSet_smul g).mono restrict_le_self)

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