English
divLeft g is a measurable equivalence on G with toEquiv = Equiv.divLeft g, measurable_toFun = measurable_id.const_div g, measurable_invFun = measurable_inv.mul_const g.
Русский
divLeft g образует измеримое эквив на G: toEquiv = Equiv.divLeft g, измеримость отображения = measurable_id.const_div g, измеримость обратного = measurable_inv.mul_const g.
LaTeX
$$$\\text{divLeft}[\\MeasurableMul G][\\MeasurableInv G](g) : G \\to^\\mathrm{meas} G$; \\\\ toEquiv = \\mathrm{Equiv.divLeft}(g),\\; \\text{measurable\\_toFun} = \\text{measurable\_id}.\\text{const\\_div}(g),\\; \\text{measurable\\_invFun} = \\text{measurable\_inv}.\\text{mul\\_const}(g)$$$
Lean4
/-- `equiv.divLeft` as a `MeasurableEquiv` -/
@[to_additive /-- `equiv.subLeft` as a `MeasurableEquiv` -/
]
def divLeft [MeasurableMul G] [MeasurableInv G] (g : G) : G ≃ᵐ G
where
toEquiv := Equiv.divLeft g
measurable_toFun := measurable_id.const_div g
measurable_invFun := measurable_inv.mul_const g
