instIsMulRightInvariantCount — Mathlib

English

The counting measure on a group G is right-invariant: for any g ∈ G and any measurable A, #(A · g) = # A.

Русский

Счётная мера на группе G справа инвариантна: для любого g и измеримого A имеет место #(A · g) = # A.

LaTeX

$$$ #(A \cdot g) = #A \quad \text{для всех } g \in G, A \text{ измеримо}$$$

Lean4

@[to_additive]
instance : (count : Measure G).IsMulRightInvariant where
  map_mul_right_eq_self
    g := by
    ext s hs
    rw [count_apply hs, map_apply (measurable_mul_const _) hs, count_apply (measurable_mul_const _ hs),
      encard_preimage_of_bijective (Group.mulRight_bijective _)]

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