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

source
@[instance_reducible]
instance Empty.instMeasurableSpace :
MeasurableSpace Empty
source
@[instance_reducible]
instance PUnit.instMeasurableSpace :
MeasurableSpace PUnit.{u_1 + 1}
source
@[instance_reducible]
instance Bool.instMeasurableSpace :
MeasurableSpace Bool
source
@[instance_reducible]
instance Prop.instMeasurableSpace :
MeasurableSpace Prop
source
@[instance_reducible]
instance Nat.instMeasurableSpace :
MeasurableSpace ℕ
source
@[instance_reducible]
instance ENat.instMeasurableSpace :
MeasurableSpace ℕ∞
source
@[instance_reducible]
instance Fin.instMeasurableSpace (n : ℕ) :
MeasurableSpace (Fin n)
source
@[instance_reducible]
instance ZMod.instMeasurableSpace (n : ℕ) :
MeasurableSpace (ZMod n)
source
@[instance_reducible]
instance Int.instMeasurableSpace :
MeasurableSpace ℤ
source
@[instance_reducible]
instance Rat.instMeasurableSpace :
MeasurableSpace ℚ
source
@[instance_reducible]
instance IterateMulAct.instMeasurableSpace {α : Type u_1} {f : α → α} :
MeasurableSpace (IterateMulAct f)
source
@[instance_reducible]
instance IterateAddAct.instMeasurableSpace {α : Type u_1} {f : α → α} :
MeasurableSpace (IterateAddAct f)
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 ℚ