shearDivRight — Mathlib

English

The map (x, y) ↦ (x, y/x) is a measurable equivalence with inverse (x, y) ↦ (x, yx).

Русский

Отображение (x, y) ↦ (x, y/x) — измеримое биекции с обратной (x, y) ↦ (x, yx).

LaTeX

$$MeasurableEquiv shearDivRight$$

Lean4

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

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