OAI/Analysis/Pureness/Divisibility/HereditaryApproximateUnit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.rootExponent_tendsto line 12
2. lemma OAI.CuntzPureness.root_mul_uniform line 18
3. lemma OAI.CuntzPureness.normalizedRoot_mul_normalize_tendsto line 48
4. lemma OAI.CuntzPureness.norm_smul_normalizePositive line 74
5. lemma OAI.CuntzPureness.normalizedRoot_mul_self_tendsto line 79
6. lemma OAI.CuntzPureness.normalizedRoot_mul_hereditary_tendsto line 84