smul_mem_ae — Mathlib

English

For any c ∈ G, the a.e. membership of a set in the measure's ae filter is preserved under smul: c•s ∈ ae μ iff s ∈ ae μ.

Русский

Для любого c ∈ G принадлежность множества в ae-множество по мере сохраняется под действием: c•s ∈ ae μ эквивалентно s ∈ ae μ.

LaTeX

$$$c\\cdot s \\in \\ae\\mu \\iff s \\in \\ae\\mu$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_mem_ae (c : G) {s : Set α} : c • s ∈ ae μ ↔ s ∈ ae μ := by
  simp only [mem_ae_iff, ← smul_set_compl, measure_smul_eq_zero_iff]

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