MIL/C11_Topology/S02_Metric_Spaces.lean

GitHub source file

33 declarations, 5 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. example (example at line 21) line 21 source
  2. example (example at line 25) line 25 source
  3. example (example at line 30) line 30 source
  4. example (example at line 33) line 33 source
  5. example (example at line 37) line 37 source
  6. example (example at line 43) line 43 source
  7. example (example at line 47) line 47 source
  8. example (example at line 51) sorry line 51 source
  9. example (example at line 53) line 53 source
  10. example (example at line 59) line 59 source
  11. example (example at line 62) line 62 source
  12. example (example at line 65) line 65 source
  13. example (example at line 68) line 68 source
  14. example (example at line 71) line 71 source
  15. example (example at line 74) line 74 source
  16. example (example at line 77) line 77 source
  17. example (example at line 81) line 81 source
  18. example (example at line 84) sorry line 84 source
  19. example (example at line 87) line 87 source
  20. example (example at line 90) line 90 source
  21. example (example at line 93) line 93 source
  22. example (example at line 96) line 96 source
  23. example (example at line 100) line 100 source
  24. example (example at line 105) line 105 source
  25. example (example at line 110) line 110 source
  26. example (example at line 113) line 113 source
  27. example (example at line 118) line 118 source
  28. example (example at line 123) sorry line 123 source
  29. example (example at line 127) line 127 source
  30. example (example at line 131) line 131 source
  31. example (example at line 135) line 135 source
  32. theorem cauchySeq_of_le_geometric_two' sorry line 143 source

    depends on sorry what this means

    Statement uses: MetricSpace, Nat, LE.le, Real, Dist.dist, HAdd.hAdd, OfNat.ofNat, HPow.hPow, HDiv.hDiv, CauchySeq

    Proof uses: Eq.mpr, GT.gt, Exists, GE.ge, LT.lt, id, Eq, congrArg, propext, Metric.cauchySeq_iff', HMul.hMul, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Exists.intro, Iff.mp, le_iff_exists_add and 4 more

    62 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C11_Topology/solutions/Solutions_S02_Metric_Spaces.lean:178 (same statement text; different proof or body). Qualify references as cauchySeq_of_le_geometric_two'@path.

    Tactic trace: 36 steps

    Open to load the checked before-and-after goal states.

  33. example (example at line 162) sorry line 162 source