eventually_mul_right_iff — Mathlib

English

For a left-invariant μ, almost everywhere statements of p(t·x) are equivalent to p(x).

Русский

Для левой инвариантности μ почти везде p(t·x) эквивалентно p(x).

LaTeX

$$$(∀^{*} x, p(t\cdot x)) \iff (∀^{*} x, p(x))$$$

Lean4

@[to_additive]
theorem eventually_mul_right_iff (μ : Measure G) [IsMulRightInvariant μ] (t : G) {p : G → Prop} :
    (∀ᵐ x ∂μ, p (x * t)) ↔ ∀ᵐ x ∂μ, p x :=
  by
  conv_rhs => rw [Filter.Eventually, ← map_mul_right_ae μ t]
  rfl

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