OAI/Probability/SpanningForest/CoordinateTruncation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.CoordinateTruncation.Space line 14
  2. def OAI.Problem336.CoordinateTruncation.truncate line 16
  3. lemma OAI.Problem336.CoordinateTruncation.truncate_eq_sum line 20
  4. theorem OAI.Problem336.CoordinateTruncation.truncate_apply line 26
  5. theorem OAI.Problem336.CoordinateTruncation.tendsto_truncate line 31
  6. def OAI.Problem336.CoordinateTruncation.supported line 38
  7. theorem OAI.Problem336.CoordinateTruncation.mem_supported line 45
  8. theorem OAI.Problem336.CoordinateTruncation.supported_mono line 49
  9. instance OAI.Problem336.CoordinateTruncation.supported_isClosed line 54
  10. instance OAI.Problem336.CoordinateTruncation.supported_completeSpace line 65
  11. instance OAI.Problem336.CoordinateTruncation.supported_hasOrthogonalProjection line 68
  12. theorem OAI.Problem336.CoordinateTruncation.single_mem_supported line 71
  13. theorem OAI.Problem336.CoordinateTruncation.supported_starProjection_apply line 77
  14. theorem OAI.Problem336.CoordinateTruncation.truncate_mem_supported line 90
  15. theorem OAI.Problem336.CoordinateTruncation.sub_truncate_mem_orthogonal line 96
  16. theorem OAI.Problem336.CoordinateTruncation.starProjection_supported line 108
  17. theorem OAI.Problem336.CoordinateTruncation.closure_iSup_supported line 115
  18. theorem OAI.Problem336.CoordinateTruncation.tendsto_truncate_supported line 140