Theorems · Definition · measure theory

MeasurableSMul.casesOn

{M : Type u_2} →
  {α : Type u_3} →
    [inst : SMul M α] →
      [inst_1 : MeasurableSpace M] →
        [inst_2 : MeasurableSpace α] →
          {motive : MeasurableSMul M α → Sort u} →
            (t : MeasurableSMul M α) →
              ([toMeasurableConstSMul : MeasurableConstSMul M α] →
                  (measurable_smul_const : ∀ (x : α), Measurable fun x_1 => x_1 • x) → motive ⋯) →
                motive t

Defined in

Mathlib.MeasureTheory.Group.Arithmetic

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

SMulMeasurableSpaceMeasurableSpace