OAI/Analysis/KadisonKastler/MeasurableImplementers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Selecting measurable implementer fields

The input is the published Borel uniformization theorem. The conjugacy relation, its Borel structure, and the strong measurability of the selected operator and adjoint evaluations are proved locally.

  1. theorem OAI.KadisonKastler.exists_measurable_implementer_field line 24