exists_map_addHaar_eq_smul_addHaar

English

The image of an additive Haar measure μ under a surjective linear map L is proportional to another additive Haar measure ν, i.e., there exists c > 0 with μ.map L = c • ν.

Русский

Образ аддитивной меры Хаара μ под сюръективным линейным отображением L пропорционален другой аддитивной мере Хаара ν: существует c > 0 такое, что μ.map L = c • ν.

LaTeX

$$$$ \exists c \; (0 < c) \wedge (\mu.map L = c \cdot \nu). $$$$

Lean4

/-- The image of an additive Haar measure under a surjective linear map is proportional to a given
additive Haar measure, with a positive (but maybe infinite) factor. -/
theorem exists_map_addHaar_eq_smul_addHaar (h : Function.Surjective L) : ∃ (c : ℝ≥0∞), 0 < c ∧ μ.map L = c • ν :=
  by
  rcases L.exists_map_addHaar_eq_smul_addHaar' μ ν h with ⟨c, c_pos, -, hc⟩
  exact ⟨_, by simp [c_pos, NeZero.ne addHaar], hc⟩

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