OAI/Analysis/KadisonKastler/UnitaryBorelSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-measure unitary selection

The Borel relation is an analytic image of Baire space. Measurable prefix hulls construct a section of its first coordinate for the given finite measure. This is the finite-measure consequence of Kechris, Classical Descriptive Set Theory, Theorems 18.1 and 21.10.

  1. theorem OAI.KadisonKastler.exists_finite_borel_selector line 23
  2. theorem OAI.KadisonKastler.publishedUnitaryBorelSelection line 57

    Source documentation

    Finite-measure selection for a Borel relation with unitary fibers.

    theorem publishedUnitaryBorelSelection : PublishedUnitaryBorelSelection.{u,v} := by
…