OAI/Analysis/CStarAlgebra/PureInfiniteness/Comparison.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MainGap.FiniteCuntzLE line 16
  2. def OAI.MainGap.scalarCorner line 21

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:14 (same declaration text).

  3. def OAI.MainGap.doubleCorner line 24

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:17 (same declaration text).

  4. def OAI.MainGap.ProperlyInfinite line 27
  5. def OAI.MainGap.PropertyP line 30
  6. def OAI.MainGap.Diagonalization line 33

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:20 (same declaration text).

  7. def OAI.MainGap.UnrestrictedDiagonalization line 39

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:26 (same declaration text).

  8. def OAI.MainGap.StronglyPurelyInfinite line 43

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:30 (same declaration text).

  9. lemma OAI.MainGap.matrix_mul_assoc line 47
  10. lemma OAI.MainGap.matrix_star_mul line 51
  11. lemma OAI.MainGap.continuous_matrix_mul line 56
  12. lemma OAI.MainGap.continuous_matrix_star line 61
  13. lemma OAI.MainGap.finiteCuntzLE_iff_closure line 67
  14. lemma OAI.MainGap.FiniteCuntzLE.exists_approx line 79
  15. lemma OAI.MainGap.finiteCuntzLE_of_forall_approx line 87
  16. lemma OAI.MainGap.FiniteCuntzLE.conjugate line 96
  17. lemma OAI.MainGap.FiniteCuntzLE.trans line 110
  18. lemma OAI.MainGap.isClosed_finiteCuntzLE line 118
  19. lemma OAI.MainGap.FiniteCuntzLE.of_tendsto line 123
  20. lemma OAI.MainGap.FiniteCuntzLE.refl line 128
  21. def OAI.MainGap.matrixBlock line 154
  22. lemma OAI.MainGap.matrixBlock_mul line 159
  23. lemma OAI.MainGap.matrixBlock_star line 173
  24. lemma OAI.MainGap.continuous_matrixBlock line 183
  25. lemma OAI.MainGap.tendsto_matrixBlock line 208
  26. lemma OAI.MainGap.matrixBlock_conjugate line 233
  27. lemma OAI.MainGap.FiniteCuntzLE.block line 240
  28. def OAI.MainGap.diagonalCorner line 257
  29. lemma OAI.MainGap.matrixBlock_diagonal line 260
  30. lemma OAI.MainGap.diagonalCorner_one line 273
  31. lemma OAI.MainGap.ProperlyInfinite.finite_copies line 279