OAI/Geometry/Borsuk/Projectors/Basic.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.projector_apply line 10
  2. theorem OAI.BorsukNine.projector_neg line 13
  3. theorem OAI.BorsukNine.continuous_projector line 17
  4. theorem OAI.BorsukNine.isCompact_projectorSet line 23
  5. theorem OAI.BorsukNine.projector_inner line 30
  6. theorem OAI.BorsukNine.projector_norm_sq line 43
  7. theorem OAI.BorsukNine.projectorSet_subset_traceOneSymmetric line 47
  8. theorem OAI.BorsukNine.projector_dist_sq line 58
  9. theorem OAI.BorsukNine.projector_dist_le line 64
  10. theorem OAI.BorsukNine.projector_dist_eq_sqrt_two_iff line 71
  11. theorem OAI.BorsukNine.diam_projectorSet line 86
  12. structure OAI.BorsukNine.Admissible line 101
  13. theorem OAI.BorsukNine.contDiff_projector line 110
  14. theorem OAI.BorsukNine.dist_lt_of_mem_thickening_small line 115
  15. theorem OAI.BorsukNine.cover_to_admissible line 135
  16. theorem OAI.BorsukNine.compact_diam_lt line 170
  17. theorem OAI.BorsukNine.admissible_to_cover line 183
  18. theorem OAI.BorsukNine.cover_iff_admissible line 220
  19. theorem OAI.BorsukNine.exists_unit_orthogonal line 224
  20. def OAI.BorsukNine.positiveSupport line 243
  21. theorem OAI.BorsukNine.mem_positiveSupport line 248
  22. lemma OAI.BorsukNine.Admissible.support_nonempty line 254
  23. lemma OAI.BorsukNine.Admissible.disjoint_supports line 263
  24. theorem OAI.BorsukNine.Admissible.exists_label_absent line 274