is_left_invariant_prehaar — Mathlib

English

The prehaar is invariant under left translation by g: prehaar(K0, U, map_g(K)) = prehaar(K0, U, K).

Русский

Prehaar не изменяется при левой трансляции на g: prehaar(K0,U, g·K) = prehaar(K0,U, K).

LaTeX

$$$\text{prehaar}_{K_0}(U, K\mapsto gK) = \text{prehaar}_{K_0}(U, K)$$$

Lean4

@[to_additive]
theorem is_left_invariant_prehaar {K₀ : PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) (g : G)
    (K : Compacts G) : prehaar (K₀ : Set G) U (K.map _ <| continuous_mul_left g) = prehaar (K₀ : Set G) U K := by
  simp only [prehaar, Compacts.coe_map, is_left_invariant_index K.isCompact _ hU]

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