measurableDiv_of_mul_inv — Mathlib

English

If the two-variable division operation is measurable on G, then the one-variable division operation is measurable as a function G → G with the variables fixed.

Русский

Если двуарное деление измеримо на G, то однозначное деление измеримо как функция G → G при фиксированных аргументах.

LaTeX

$$$\\text{MeasurableDiv G}$$$

Lean4

@[to_additive]
instance (priority := 100) measurableDiv_of_mul_inv (G : Type*) [MeasurableSpace G] [DivInvMonoid G] [MeasurableMul G]
    [MeasurableInv G] : MeasurableDiv G
    where
  measurable_const_div
    c := by
    convert measurable_inv.const_mul c using 1
    ext1
    apply div_eq_mul_inv
  measurable_div_const
    c := by
    convert measurable_id.mul_const c⁻¹ using 1
    ext1
    apply div_eq_mul_inv

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