OAI/Geometry/Convex/GeneralMahler/Frame/Selector.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Borel selection for a closed relation into a compact metric space.

  1. def OAI.GeneralMahler.Select.near line 13
  2. lemma OAI.GeneralMahler.Select.near_m line 15
  3. def OAI.GeneralMahler.Select.eps line 24
  4. lemma OAI.GeneralMahler.Select.dense_approx line 26
  5. lemma OAI.GeneralMahler.Select.choose_m line 30
  6. abbrev OAI.GeneralMahler.Select.tag line 38
  7. lemma OAI.GeneralMahler.Select.start line 40
  8. lemma OAI.GeneralMahler.Select.next line 48
  9. theorem OAI.GeneralMahler.Select.selector line 64