The Borel structure of SU(2) #
SU(2) carries the subspace topology of the 2 × 2 complex matrices, which makes it a compact
Hausdorff topological group (TauCeti/RepresentationTheory/SU2/Basic.lean), but no measurable
structure comes with it. This file equips it with its Borel σ-algebra, which is what lets the Haar
measure of a compact group -- and with it the L² theory of
TauCeti/RepresentationTheory/Compact/ -- be applied to SU(2).
The σ-algebra is taken to be borel SU(2) by definition, so the MeasurableSpace and
BorelSpace instances agree by construction and no compatibility lemma is needed.
@[instance_reducible]
SU(2) carries its Borel σ-algebra, the measurable structure Haar measure needs.