MIL/C11_Topology/solutions/Solutions_S02_Metric_Spaces.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
  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) line 51 source
  9. example (example at line 55) line 55 source
  10. example (example at line 61) line 61 source
  11. example (example at line 64) line 64 source
  12. example (example at line 67) line 67 source
  13. example (example at line 70) line 70 source
  14. example (example at line 73) line 73 source
  15. example (example at line 76) line 76 source
  16. example (example at line 79) line 79 source
  17. example (example at line 83) line 83 source
  18. example (example at line 86) line 86 source
  19. example (example at line 97) line 97 source
  20. example (example at line 100) line 100 source
  21. example (example at line 103) line 103 source
  22. example (example at line 106) line 106 source
  23. example (example at line 110) line 110 source
  24. example (example at line 115) line 115 source
  25. example (example at line 120) line 120 source
  26. example (example at line 123) line 123 source
  27. example (example at line 128) line 128 source
  28. example (example at line 133) line 133 source
  29. example (example at line 162) line 162 source
  30. example (example at line 166) line 166 source
  31. example (example at line 170) line 170 source
  32. theorem cauchySeq_of_le_geometric_two' line 178 source

    standard axioms: Classical.choice, Quot.sound, propext 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, Filter.Tendsto, Filter.atTop, nhds, Eq.symm, MulZeroClass.zero_mul, Filter.Tendsto.mul, congrFun', Filter, funext and 110 more

    182 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 82 steps

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

  33. example (example at line 208) line 208 source