measure_mul_closure_one — Mathlib

English

μ(s * closure{1}) = μ(s) for any measurable s.

Русский

μ(s ⋅ closure{1}) = μ(s) для любого измеримого s.

LaTeX

$$$\mu(s \cdot \overline{\{1\}}) = \mu(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem measure_mul_closure_one (s : Set G) (μ : Measure G) : μ (s * (closure { 1 } : Set G)) = μ s :=
  by
  apply le_antisymm ?_ (measure_mono (subset_mul_closure_one s))
  conv_rhs => rw [measure_eq_iInf]
  simp only [le_iInf_iff]
  intro t kt t_meas
  apply measure_mono
  rw [← t_meas.mul_closure_one_eq]
  exact smul_subset_smul_right kt

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