MIL/C11_Topology/S03_Topological_Spaces.lean

GitHub source file

31 declarations, 4 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. example (example at line 10) line 10 source
  2. example (example at line 13) line 13 source
  3. example (example at line 16) line 16 source
  4. example (example at line 19) line 19 source
  5. example (example at line 25) line 25 source
  6. example (example at line 28) line 28 source
  7. example (example at line 31) line 31 source
  8. example (example at line 34) line 34 source
  9. example (example at line 37) line 37 source
  10. example (example at line 40) line 40 source
  11. example (example at line 43) line 43 source
  12. example (example at line 50) sorry line 50 source
  13. example (example at line 58) line 58 source
  14. example (example at line 61) line 61 source
  15. example (example at line 64) line 64 source
  16. example (example at line 72) line 72 source
  17. example (example at line 75) line 75 source
  18. example (example at line 79) line 79 source
  19. example (example at line 85) line 85 source
  20. example (example at line 90) line 90 source
  21. example (example at line 94) line 94 source
  22. example (example at line 98) line 98 source
  23. theorem aux sorry line 102 source

    depends on sorry what this means

    Statement uses: TopologicalSpace, Filter, Filter.Tendsto, Filter.comap, nhds, Set, Membership.mem, Exists, And, IsOpen, HasSubset.Subset, Set.preimage

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    5 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean:171 (different declaration text), MIL/C11_Topology/solutions/Solutions_S03_Topological_Spaces.lean:106 (same statement text; different proof or body). Qualify references as aux@path.

    Tactic trace: 9 steps

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

  24. example (example at line 108) sorry line 108 source
  25. example (example at line 116) line 116 source
  26. example (example at line 123) line 123 source
  27. example (example at line 126) line 126 source
  28. example (example at line 130) line 130 source
  29. example (example at line 136) line 136 source
  30. example (example at line 140) sorry line 140 source
  31. example (example at line 148) line 148 source