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 ENat.instMeasurableSpace : MeasurableSpace ℕ∞

Equations

• ENat.instMeasurableSpace = ⊤

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

Equations

• Fin.instMeasurableSpace n = ⊤

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

Equations

• ZMod.instMeasurableSpace n = ⊤

instance Int.instMeasurableSpace : MeasurableSpace ℤ

Equations

• Int.instMeasurableSpace = ⊤

instance Rat.instMeasurableSpace : MeasurableSpace ℚ

Equations

• Rat.instMeasurableSpace = ⊤

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

Equations

• IterateMulAct.instMeasurableSpace = ⊤

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

Equations

• IterateAddAct.instMeasurableSpace = ⊤

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

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 ENat.instDiscreteMeasurableSpace : DiscreteMeasurableSpace ℕ∞

Equations

• ENat.instDiscreteMeasurableSpace = ⋯

instance ENat.instMeasurableSingletonClass : MeasurableSingletonClass ℕ∞

Equations

• ENat.instMeasurableSingletonClass = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Int.instMeasurableSingletonClass : MeasurableSingletonClass ℤ

Equations

• Int.instMeasurableSingletonClass = ⋯

instance Rat.instMeasurableSingletonClass : MeasurableSingletonClass ℚ

Equations

• Rat.instMeasurableSingletonClass = ⋯