OAI/Analysis/SeparableQuotients/Positive/FiniteSuppression.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.Positive.Sampling.exists_halfNormer line 15
2. def OAI.SeparableQuotient.Positive.Sampling.halfNormer line 25
3. lemma OAI.SeparableQuotient.Positive.Sampling.halfNormer_zero line 28
4. lemma OAI.SeparableQuotient.Positive.Sampling.norm_halfNormer line 31
5. lemma OAI.SeparableQuotient.Positive.Sampling.halfNormer_bound line 36
6. abbrev OAI.SeparableQuotient.Positive.Sampling.UnitBall line 41
7. def OAI.SeparableQuotient.Positive.Sampling.ballHalfNormer line 42
8. lemma OAI.SeparableQuotient.Positive.Sampling.suppression_of_cross_vanishing line 45