OAI/MeasureTheory/Falconer/Radial/TubeCoverChoice.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable choice of countably listed original-label tube covers

  1. theorem OAI.Falconer.tube_cover_uncovered_mass_measurable line 12
  2. theorem OAI.Falconer.exists_measurable_tube_cover_choice line 22