measurePreserving_prod_mul_swap_right

English

The map (x,y) ↦ (y, x·y) sends μ×ν to ν×μ when μ is invariant under right multiplication.

Русский

Отображение (x,y) ↦ (y, x·y) переводит меру μ×ν в ν×μ при инвариантности μ относительно правого умножения.

LaTeX

$$$\text{MeasurePreserving}(\lambda z. (z.2, z.1 * z.2),\ (\mu \prod ν), (ν \prod μ))$$$

Lean4

/-- The map `(x, y) ↦ (y, xy)` sends the measure `μ × ν` to `ν × μ`. -/
@[to_additive measurePreserving_prod_add_swap_right /--
    The map `(x, y) ↦ (y, x + y)` sends the measure `μ × ν` to `ν × μ`. -/
    ]
theorem measurePreserving_prod_mul_swap_right [IsMulRightInvariant μ] :
    MeasurePreserving (fun z : G × G => (z.2, z.1 * z.2)) (μ.prod ν) (ν.prod μ) :=
  (measurePreserving_prod_mul_right ν μ).comp measurePreserving_swap

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