smul_set_ae_le — Mathlib

English

For any c ∈ G, and sets s,t, the almost-everywhere relation between smul-sets is equivalent to the relation between the originals: c•s ≤ᵐ c•t iff s ≤ᵐ t.

Русский

Для любого c ∈ G и множеств s,t равенство ae-отношения между c•s и c•t эквивалентно ae-отношению между s и t.

LaTeX

$$$c\\;s \\leq^{\\ae}_{\\mu} c\\;t \\iff s \\leq^{\\ae}_{\\mu} t$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_set_ae_le (c : G) {s t : Set α} : c • s ≤ᵐ[μ] c • t ↔ s ≤ᵐ[μ] t := by
  simp only [ae_le_set, ← smul_set_sdiff, measure_smul_eq_zero_iff]

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