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_reducible]

instance Empty.instMeasurableSpace : MeasurableSpace Empty

Equations

• Empty.instMeasurableSpace = ⊤

@[instance_reducible]

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

Equations

• PUnit.instMeasurableSpace = ⊤

@[instance_reducible]

instance Bool.instMeasurableSpace : MeasurableSpace Bool

Equations

• Bool.instMeasurableSpace = ⊤

@[instance_reducible]

instance Prop.instMeasurableSpace : MeasurableSpace Prop

Equations

• «Prop».instMeasurableSpace = ⊤

@[instance_reducible]

instance Nat.instMeasurableSpace : MeasurableSpace ℕ

Equations

• Nat.instMeasurableSpace = ⊤

@[instance_reducible]

instance ENat.instMeasurableSpace : MeasurableSpace ℕ∞

Equations

• ENat.instMeasurableSpace = ⊤

@[instance_reducible]

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

Equations

• Fin.instMeasurableSpace n = ⊤

@[instance_reducible]

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

Equations

• ZMod.instMeasurableSpace n = ⊤

@[instance_reducible]

instance Int.instMeasurableSpace : MeasurableSpace ℤ

Equations

• Int.instMeasurableSpace = ⊤

@[instance_reducible]

instance Rat.instMeasurableSpace : MeasurableSpace ℚ

Equations

• Rat.instMeasurableSpace = ⊤

@[instance_reducible]

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

Equations

• IterateMulAct.instMeasurableSpace = ⊤

@[instance_reducible]

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

Equations

• IterateAddAct.instMeasurableSpace = ⊤

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 ℚ