OAI/Analysis/SeparableQuotients/Positive/MeasurableCodes.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SeparableQuotient.Positive.Sampling.WeakUnitBall line 15
  2. instance OAI.SeparableQuotient.Positive.Sampling.weakUnitBallCompact line 17
  3. instance OAI.SeparableQuotient.Positive.Sampling.weakUnitBallMetrizable line 23
  4. instance OAI.SeparableQuotient.Positive.Sampling.weakUnitBallSecondCountable line 26
  5. instance OAI.SeparableQuotient.Positive.Sampling.weakUnitBallMeasurable line 29
  6. instance OAI.SeparableQuotient.Positive.Sampling.weakUnitBallBorel line 30
  7. lemma OAI.SeparableQuotient.Positive.Sampling.continuous_weakUnitBall_eval line 32
  8. lemma OAI.SeparableQuotient.Positive.Sampling.continuous_sequence_eval line 55
  9. lemma OAI.SeparableQuotient.Positive.Sampling.measurable_sequence_eval line 60
  10. def OAI.SeparableQuotient.Positive.Sampling.limitOrZero line 64
  11. lemma OAI.SeparableQuotient.Positive.Sampling.limitOrZero_of_tendsto line 68
  12. lemma OAI.SeparableQuotient.Positive.Sampling.limitOrZero_of_not_tendsto line 73
  13. lemma OAI.SeparableQuotient.Positive.Sampling.measurable_limitOrZero line 78
  14. def OAI.SeparableQuotient.Positive.Sampling.evaluation line 105
  15. lemma OAI.SeparableQuotient.Positive.Sampling.evaluation_apply line 108
  16. lemma OAI.SeparableQuotient.Positive.Sampling.norm_evaluation_le line 111
  17. def OAI.SeparableQuotient.Positive.Sampling.evaluationBall line 116
  18. def OAI.SeparableQuotient.Positive.Sampling.sequentialCodeValue line 126
  19. lemma OAI.SeparableQuotient.Positive.Sampling.measurable_sequentialCodeValue line 129
  20. lemma OAI.SeparableQuotient.Positive.Sampling.sequentialCodeValue_eq line 137
  21. lemma OAI.SeparableQuotient.Positive.Sampling.sequentialCodeValue_evaluation line 143