OAI/Analysis/CStarAlgebra/PureInfiniteness/Representation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MainGap.exists_complex_ultralimit line 14
  2. def OAI.MainGap.ultraValue line 28
  3. lemma OAI.MainGap.tendsto_ultraValue line 31
  4. def OAI.MainGap.ultraPositive line 35
  5. lemma OAI.MainGap.tendsto_ultraPositive line 49
  6. lemma OAI.MainGap.ultraPositive_norm_le line 53
  7. lemma OAI.MainGap.ultraPositive_eq_zero_of_tendsto line 56
  8. lemma OAI.MainGap.gns_zero_of_sandwich line 66
  9. lemma OAI.MainGap.gnsStar_nonzero_of_value line 79
  10. def OAI.MainGap.vectorPositive line 103
  11. lemma OAI.MainGap.vectorPositive_norm_le line 113
  12. lemma OAI.MainGap.vectorPositive_star_mul line 124
  13. def OAI.MainGap.limitFunctional line 139
  14. abbrev OAI.MainGap.LimitHilbert line 143
  15. def OAI.MainGap.limitRep line 145
  16. lemma OAI.MainGap.limitFunctional_tendsto line 148
  17. lemma OAI.MainGap.limitRep_annihilates line 152
  18. lemma OAI.MainGap.limitRep_nonzero line 174
  19. def OAI.MainGap.generatedRange line 199
  20. instance OAI.MainGap.(instance at line 202) line 202
  21. lemma OAI.MainGap.range_mem_generatedRange line 206
  22. lemma OAI.MainGap.generatedRange_invariant line 211
  23. def OAI.MainGap.rangeRestriction line 222
  24. lemma OAI.MainGap.rangeRestriction_apply line 239
  25. lemma OAI.MainGap.rangeRestriction_kills line 242
  26. lemma OAI.MainGap.rangeRestriction_nonzero line 255