shearMulRight — Mathlib

English

The shear map (x, y) ↦ (x, xy) is a measurable equivalence with measurable inverse (x, y) ↦ (x, x⁻¹y).

Русский

Сдвиг по правой части (x, y) ↦ (x, xy) задаёт измеримую взаимно однозначную связь с обратной функцией (x, y) ↦ (x, x⁻¹y).

LaTeX

$$MeasurableEquiv shearMulRight$$

Lean4

/-- The map `(x, y) ↦ (x, xy)` as a `MeasurableEquiv`. -/
@[to_additive /-- The map `(x, y) ↦ (x, x + y)` as a `MeasurableEquiv`. -/
    ]
protected def shearMulRight [MeasurableInv G] : G × G ≃ᵐ G × G :=
  {
    Equiv.prodShear (Equiv.refl _)
      Equiv.mulLeft with
    measurable_toFun := measurable_fst.prodMk measurable_mul
    measurable_invFun := measurable_fst.prodMk <| measurable_fst.inv.mul measurable_snd }

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