measurableDiv₂_of_mul_inv — Mathlib

English

The map (a,b) ↦ a / b is measurable on G × G when G has a DivInvMonoid structure with MeasurableMul and MeasurableInv.

Русский

Отображение (a,b) ↦ a / b по произведению G × G измеримо при наличии структуры DivInvMonoid и измеримой умножения и инверсии.

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 :=
  ⟨by
    simp only [div_eq_mul_inv]
    exact measurable_fst.mul measurable_snd.inv⟩
    -- See note [lower instance priority]

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