OAI/Analysis/Pureness/Comparison/Fullness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzComparison.finiteSandwichIdeal line 11
  2. theorem OAI.CuntzComparison.mem_finiteSandwichIdeal line 37
  3. def OAI.CuntzComparison.closedTwoSidedIdeal line 42
  4. theorem OAI.CuntzComparison.coe_closedTwoSidedIdeal line 67
  5. theorem OAI.CuntzComparison.full_of_ne_zero line 71
  6. theorem OAI.CuntzComparison.exists_finite_fullness_approximation line 85
  7. theorem OAI.CuntzComparison.exists_finite_fullness_identity line 94
  8. theorem OAI.CuntzComparison.exists_nonzero_sandwich line 109