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

source
instance Empty.instMeasurableSpace :
MeasurableSpace Empty
Equations

- Empty.instMeasurableSpace = ⊤

source
instance PUnit.instMeasurableSpace :
MeasurableSpace PUnit.{u_1 + 1}
Equations

- PUnit.instMeasurableSpace = ⊤

source
instance Bool.instMeasurableSpace :
MeasurableSpace Bool
Equations

- Bool.instMeasurableSpace = ⊤

source
instance Prop.instMeasurableSpace :
MeasurableSpace Prop
Equations

- «Prop».instMeasurableSpace = ⊤

source
instance Nat.instMeasurableSpace :
MeasurableSpace ℕ
Equations

- Nat.instMeasurableSpace = ⊤

source
instance ENat.instMeasurableSpace :
MeasurableSpace ℕ∞
Equations

- ENat.instMeasurableSpace = ⊤

source
instance Fin.instMeasurableSpace (n : ℕ) :
MeasurableSpace (Fin n)
Equations

- Fin.instMeasurableSpace n = ⊤

source
instance ZMod.instMeasurableSpace (n : ℕ) :
MeasurableSpace (ZMod n)
Equations

- ZMod.instMeasurableSpace n = ⊤

source
instance Int.instMeasurableSpace :
MeasurableSpace ℤ
Equations

- Int.instMeasurableSpace = ⊤

source
instance Rat.instMeasurableSpace :
MeasurableSpace ℚ
Equations

- Rat.instMeasurableSpace = ⊤

source
instance IterateMulAct.instMeasurableSpace {α : Type u_1} {f : α → α} :
MeasurableSpace (IterateMulAct f)
Equations

- IterateMulAct.instMeasurableSpace = ⊤

source
instance IterateAddAct.instMeasurableSpace {α : Type u_1} {f : α → α} :
MeasurableSpace (IterateAddAct f)
Equations

- IterateAddAct.instMeasurableSpace = ⊤

source
instance IterateMulAct.instDiscreteMeasurableSpace {α : Type u_1} {f : α → α} :
DiscreteMeasurableSpace (IterateMulAct f)
source
instance IterateAddAct.instDiscreteMeasurableSpace {α : Type u_1} {f : α → α} :
DiscreteMeasurableSpace (IterateAddAct f)
source
@[instance 100]
instance Subsingleton.measurableSingletonClass {α : Type u_1} [MeasurableSpace α] [Subsingleton α] :
MeasurableSingletonClass α
source
instance Bool.instMeasurableSingletonClass :
MeasurableSingletonClass Bool
source
instance Prop.instMeasurableSingletonClass :
MeasurableSingletonClass Prop
source
instance Nat.instMeasurableSingletonClass :
MeasurableSingletonClass ℕ
source
instance ENat.instDiscreteMeasurableSpace :
DiscreteMeasurableSpace ℕ∞
source
instance ENat.instMeasurableSingletonClass :
MeasurableSingletonClass ℕ∞
source
instance Fin.instMeasurableSingletonClass (n : ℕ) :
MeasurableSingletonClass (Fin n)
source
instance ZMod.instMeasurableSingletonClass (n : ℕ) :
MeasurableSingletonClass (ZMod n)
source
instance Int.instMeasurableSingletonClass :
MeasurableSingletonClass ℤ
source
instance Rat.instMeasurableSingletonClass :
MeasurableSingletonClass ℚ