OAI/Geometry/Borsuk/Projectors/CompactTargetHits.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BorsukNine.compact_target_hits line 9
  2. def OAI.BorsukNine.balancedModel line 37
  3. lemma OAI.BorsukNine.balancedModel_continuous line 44
  4. def OAI.BorsukNine.modelChambers line 52
  5. lemma OAI.BorsukNine.modelChambers_open line 57
  6. lemma OAI.BorsukNine.modelChambers_disjoint line 62
  7. lemma OAI.BorsukNine.modelChambers_cover line 70
  8. def OAI.BorsukNine.levelHomotopy line 78
  9. lemma OAI.BorsukNine.levelHomotopy_eq line 85
  10. lemma OAI.BorsukNine.Admissible.levelHomotopy_continuousOn line 96
  11. lemma OAI.BorsukNine.Admissible.level_hits_compact line 119