smul_ae — Mathlib

English

For any c, the a.e. equality of two sets is preserved after applying c•: c•s = ae μ c•t iff s = ae μ t.

Русский

Для любого c сохраняется эквивалентность по ae после применения c•: c•s = ae μ c•t ⇔ s = ae μ t.

LaTeX

$$$c\\cdot s =_{\\ae\\mu} c\\cdot t \\iff s =_{\\ae\\mu} t$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_ae (c : G) : c • ae μ = ae μ := by
  ext s
  simp only [mem_smul_filter, preimage_smul, smul_mem_ae]

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