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).
Equations
Equations
Equations
Equations
Equations
@[instance 100]
instance
Subsingleton.measurableSingletonClass
{α : Type u_1}
[MeasurableSpace α]
[Subsingleton α]
: