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).

@[implicit_reducible]

instance Empty.instMeasurableSpace :

MeasurableSpace Empty

@[implicit_reducible]

instance PUnit.instMeasurableSpace :

MeasurableSpace PUnit.{u_1 + 1}

@[implicit_reducible]

instance Bool.instMeasurableSpace :

MeasurableSpace Bool

@[implicit_reducible]

instance Prop.instMeasurableSpace :

MeasurableSpace Prop

@[implicit_reducible]

instance Nat.instMeasurableSpace :

MeasurableSpace ℕ

@[implicit_reducible]

instance ENat.instMeasurableSpace :

MeasurableSpace ℕ∞

@[implicit_reducible]

instance Fin.instMeasurableSpace (n : ℕ) :

MeasurableSpace (Fin n)

@[implicit_reducible]

instance ZMod.instMeasurableSpace (n : ℕ) :

MeasurableSpace (ZMod n)

@[implicit_reducible]

instance Int.instMeasurableSpace :

MeasurableSpace ℤ

@[implicit_reducible]

instance Rat.instMeasurableSpace :

MeasurableSpace ℚ

@[implicit_reducible]

instance IterateMulAct.instMeasurableSpace {α : Type u_1} {f : α → α} :

MeasurableSpace (IterateMulAct f)

@[implicit_reducible]

instance IterateAddAct.instMeasurableSpace {α : Type u_1} {f : α → α} :

MeasurableSpace (IterateAddAct f)

instance IterateMulAct.instDiscreteMeasurableSpace {α : Type u_1} {f : α → α} :

DiscreteMeasurableSpace (IterateMulAct f)

instance IterateAddAct.instDiscreteMeasurableSpace {α : Type u_1} {f : α → α} :

DiscreteMeasurableSpace (IterateAddAct f)

@[instance 100]

instance Subsingleton.measurableSingletonClass {α : Type u_1} [MeasurableSpace α] [Subsingleton α] :

MeasurableSingletonClass α

instance Bool.instMeasurableSingletonClass :

MeasurableSingletonClass Bool

instance Prop.instMeasurableSingletonClass :

MeasurableSingletonClass Prop

instance Nat.instMeasurableSingletonClass :

MeasurableSingletonClass ℕ

instance ENat.instDiscreteMeasurableSpace :

DiscreteMeasurableSpace ℕ∞

instance ENat.instMeasurableSingletonClass :

MeasurableSingletonClass ℕ∞

instance Fin.instMeasurableSingletonClass (n : ℕ) :

MeasurableSingletonClass (Fin n)

instance ZMod.instMeasurableSingletonClass (n : ℕ) :

MeasurableSingletonClass (ZMod n)

instance Int.instMeasurableSingletonClass :

MeasurableSingletonClass ℤ

instance Rat.instMeasurableSingletonClass :

MeasurableSingletonClass ℚ