OAI/Analysis/Pureness/Stabilization/BoundedFamilies.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CuntzTrace.BoundedFamilies line 14
  2. lemma OAI.CuntzTrace.BoundedFamilies.norm_coordinate_le line 17
  3. def OAI.CuntzTrace.BoundedFamilies.vanishing line 20
  4. lemma OAI.CuntzTrace.BoundedFamilies.mem_vanishing line 30
  5. lemma OAI.CuntzTrace.BoundedFamilies.mul_mem_vanishing_left line 33
  6. lemma OAI.CuntzTrace.BoundedFamilies.mul_mem_vanishing_right line 42
  7. lemma OAI.CuntzTrace.BoundedFamilies.star_mem_vanishing line 51
  8. instance OAI.CuntzTrace.BoundedFamilies.vanishing_closed line 55
  9. def OAI.CuntzTrace.BoundedFamilies.vanishingCon line 72