OAI/Analysis/CStarAlgebra/PureInfiniteness/FourChoices.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MainGap.finite_four_choices line 14
  2. lemma OAI.MainGap.map_cut_sa line 67
  3. lemma OAI.MainGap.map_ramp_sa line 73
  4. lemma OAI.MainGap.map_deficiency line 79
  5. lemma OAI.MainGap.map_sqrt line 85
  6. lemma OAI.MainGap.map_firstX line 89
  7. lemma OAI.MainGap.map_firstV line 91
  8. lemma OAI.MainGap.map_firstH line 93
  9. lemma OAI.MainGap.map_firstK line 95
  10. lemma OAI.MainGap.map_firstU line 98
  11. lemma OAI.MainGap.map_firstR line 103
  12. lemma OAI.MainGap.map_scalingComplement line 111
  13. lemma OAI.MainGap.map_scalingDefect line 115
  14. lemma OAI.MainGap.scalingDefect_selfAdjoint line 120
  15. lemma OAI.MainGap.prospective_input_selfAdjoint line 123
  16. lemma OAI.MainGap.map_prospectiveDefect line 129
  17. lemma OAI.MainGap.map_lastX line 137
  18. lemma OAI.MainGap.map_lastR line 143
  19. structure OAI.MainGap.FourChoice line 157
  20. theorem OAI.MainGap.fourChoice_nonempty line 173
  21. lemma OAI.MainGap.firstH_fixes_V line 180
  22. lemma OAI.MainGap.FourChoice.first_mem line 186
  23. lemma OAI.MainGap.FourChoice.first_support₀ line 193
  24. lemma OAI.MainGap.FourChoice.first_support₁ line 198
  25. lemma OAI.MainGap.FourChoice.last_support line 203
  26. lemma OAI.MainGap.FourChoice.first_bound line 218
  27. lemma OAI.MainGap.FourChoice.last_bound line 228
  28. lemma OAI.MainGap.FourChoice.first_norm line 238
  29. lemma OAI.MainGap.FourChoice.last_norm_lt line 249