aeconst_of_dense_setOf_preimage_smul_eq

English

If a null-measurable set is a.e. equal to all its smul-preimages along a dense set, then ae-const.

Русский

Если нуль-измеримое множество эквивалентно своим предобразам под действием плотной множества элементов, то ae-константно.

LaTeX

$$$\text{aeconst\_of\_dense\_setOf\_preimage\_smul\_ae}\ G\ hsm hd$$

Lean4

@[to_additive]
theorem aeconst_of_dense_setOf_preimage_smul_eq (hsm : NullMeasurableSet s μ) (hd : Dense {g : M | (g • ·) ⁻¹' s = s}) :
    EventuallyConst s (ae μ) :=
  aeconst_of_dense_setOf_preimage_smul_ae hsm <| hd.mono fun _ h ↦ mem_setOf.2 <| .of_eq h

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