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

• Empty.instMeasurableSpace = ⊤

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

Equations

• PUnit.instMeasurableSpace = ⊤

instance Bool.instMeasurableSpace : MeasurableSpace Bool

Equations

• Bool.instMeasurableSpace = ⊤

instance Prop.instMeasurableSpace : MeasurableSpace Prop

Equations

• Prop.instMeasurableSpace = ⊤

instance Nat.instMeasurableSpace : MeasurableSpace ℕ

Equations

• Nat.instMeasurableSpace = ⊤

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

Equations

• Fin.instMeasurableSpace n = ⊤

instance Int.instMeasurableSpace : MeasurableSpace ℤ

Equations

• Int.instMeasurableSpace = ⊤

instance Rat.instMeasurableSpace : MeasurableSpace ℚ

Equations

• Rat.instMeasurableSpace = ⊤

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

Equations

• ⋯ = ⋯

instance Bool.instMeasurableSingletonClass : MeasurableSingletonClass Bool

Equations

• Bool.instMeasurableSingletonClass = ⋯

instance Prop.instMeasurableSingletonClass : MeasurableSingletonClass Prop

Equations

• Prop.instMeasurableSingletonClass = ⋯

instance Nat.instMeasurableSingletonClass : MeasurableSingletonClass ℕ

Equations

• Nat.instMeasurableSingletonClass = ⋯

instance Fin.instMeasurableSingletonClass (n : ℕ) : MeasurableSingletonClass (Fin n)

Equations

• ⋯ = ⋯

instance Int.instMeasurableSingletonClass : MeasurableSingletonClass ℤ

Equations

• Int.instMeasurableSingletonClass = ⋯

instance Rat.instMeasurableSingletonClass : MeasurableSingletonClass ℚ

Equations

• Rat.instMeasurableSingletonClass = ⋯