OAI/Computability/PerfectCompleteness/Algebra/UniformLinearImage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.UniformLinearImage.eq_uniform_of_weight_constant line 17
  2. theorem OAI.PerfectCompleteness.UniformLinearImage.uniform_pushforward_weight line 33
  3. theorem OAI.PerfectCompleteness.UniformLinearImage.uniform_pushforward_addHom line 48
  4. theorem OAI.PerfectCompleteness.UniformLinearImage.uniform_pushforward_linearMap line 58
  5. theorem OAI.PerfectCompleteness.UniformLinearImage.law_uniform line 69
  6. def OAI.PerfectCompleteness.UniformLinearImage.linearSum line 82
  7. theorem OAI.PerfectCompleteness.UniformLinearImage.linearSum_apply line 89
  8. theorem OAI.PerfectCompleteness.UniformLinearImage.product_uniform_linear_image line 94
  9. theorem OAI.PerfectCompleteness.UniformLinearImage.product_uniform_sum_image line 101