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 Empty.instMeasurableSpace :

MeasurableSpace Empty

Equations

instance PUnit.instMeasurableSpace :

MeasurableSpace PUnit.{u_1 + 1}

Equations

instance Bool.instMeasurableSpace :

MeasurableSpace Bool

Equations

instance Prop.instMeasurableSpace :

MeasurableSpace Prop

Equations

instance Nat.instMeasurableSpace :

MeasurableSpace ℕ

Equations

instance ENat.instMeasurableSpace :

MeasurableSpace ℕ∞

Equations

instance Fin.instMeasurableSpace (n : ℕ) :

MeasurableSpace (Fin n)

Equations

instance ZMod.instMeasurableSpace (n : ℕ) :

MeasurableSpace (ZMod n)

Equations

instance Int.instMeasurableSpace :

MeasurableSpace ℤ

Equations

instance Rat.instMeasurableSpace :

MeasurableSpace ℚ

Equations

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

MeasurableSpace (IterateMulAct f)

Equations

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

MeasurableSpace (IterateAddAct f)

Equations

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 ℚ