OAI/Analysis/Pureness/Stabilization/FamilyNorm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzTrace.BoundedFamilies.norm_bounded line 10
2. lemma OAI.CuntzTrace.BoundedFamilies.norm_cobounded line 13
3. lemma OAI.CuntzTrace.BoundedFamilies.limsup_norm_nonneg line 17
4. lemma OAI.CuntzTrace.BoundedFamilies.limsup_norm_le_of_vanishing_sub line 21
5. def OAI.CuntzTrace.BoundedFamilies.tail line 35
6. lemma OAI.CuntzTrace.BoundedFamilies.tail_sub_mem line 42
7. lemma OAI.CuntzTrace.BoundedFamilies.norm_tail_le line 48
8. theorem OAI.CuntzTrace.FamilyQuotient.norm_mk_eq_limsup line 60
9. lemma OAI.CuntzTrace.FamilyQuotient.norm_star_mul_self_eq line 77
10. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 95) line 95
11. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 98) line 98