eventually_div_right_iff — Mathlib

English

For a right-invariant μ, almost everywhere statements of p(x/x0) are equivalent to p(x).

Русский

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

LaTeX

$$$(∀^{*} x, p(x/x_0)) \iff (∀^{*} x, p(x))$$$

Lean4

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

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