Documentation

Mathlib.MeasureTheory.Constructions.AddChar

Measurable space instance for additive characters #

This file endows AddChar A M with the discrete measurable space structure whenever A is a finite discrete measurable space.

TODO #

Give the definition in the correct generality.

source
instance AddChar.instMeasurableSpace {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] [MeasurableSpace A] [DiscreteMeasurableSpace A] [Finite A] :
MeasurableSpace (AddChar A M)
Equations
  • AddChar.instMeasurableSpace = ⊤
source
instance AddChar.instDiscreteMeasurableSpace {A : Type u_1} {M : Type u_2} [AddMonoid A] [Monoid M] [MeasurableSpace A] [DiscreteMeasurableSpace A] [Finite A] :
DiscreteMeasurableSpace (AddChar A M)