instIsMulLeftInvariantCount — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance : (count : Measure G).IsMulLeftInvariant where
  map_mul_left_eq_self
    g := by
    ext s hs
    rw [count_apply hs, map_apply (measurable_const_mul _) hs, count_apply (measurable_const_mul _ hs),
      encard_preimage_of_bijective (Group.mulLeft_bijective _)]

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