Documentation

Mathlib.MeasureTheory.MeasurableSpace.Instances

Measurable-space typeclass instances #

This file provides measurable-space instances for a selection of standard countable types, in each case defining the Σ-algebra to be (the discrete measurable-space structure).

instance IterateMulAct.instMeasurableSpace {α : Type u_1} {f : αα} :
Equations
  • IterateMulAct.instMeasurableSpace =
instance IterateAddAct.instMeasurableSpace {α : Type u_1} {f : αα} :
Equations
  • IterateAddAct.instMeasurableSpace =