Mathlib Map

Structures · Analysis

MeasurableSMul

We say that the action of M on α has MeasurableSMul if for each c the map x ↦ c • x is a measurable function and for each x the map c ↦ c • x is a measurable function.

Defined in
Mathlib.MeasureTheory.Group.Arithmetic
Shape
2 explicit arguments · adds measurable_smul_const
Open in Mathlib docs

Extends1

Extended by0

Nothing extends this class yet.

Concrete types that are instances4

  • NNReal
  • Units
  • Subtype
  • MulOpposite

How is a type an instance?

Loading the hierarchy index…

Assumed by10

Ancestors1