MIL/C11_Topology/solutions/Solutions_S03_Topological_Spaces.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
  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) line 50 source
  13. example (example at line 62) line 62 source
  14. example (example at line 65) line 65 source
  15. example (example at line 68) line 68 source
  16. example (example at line 76) line 76 source
  17. example (example at line 79) line 79 source
  18. example (example at line 83) line 83 source
  19. example (example at line 89) line 89 source
  20. example (example at line 94) line 94 source
  21. example (example at line 98) line 98 source
  22. example (example at line 102) line 102 source
  23. theorem aux line 106 source

    standard axioms: Quot.sound, propext what this means

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

    Proof uses: Eq.mp, Set.MapsTo, congrArg, funext, Iff.mp, Filter.HasBasis.tendsto_left_iff, Filter.HasBasis.comap, nhds_basis_opens'

    4 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/S03_Topological_Spaces.lean:102 (same statement text; different proof or body). Qualify references as aux@path.

    Tactic trace: 36 steps

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

  24. example (example at line 112) line 112 source
  25. example (example at line 136) line 136 source
  26. example (example at line 143) line 143 source
  27. example (example at line 146) line 146 source
  28. example (example at line 150) line 150 source
  29. example (example at line 156) line 156 source
  30. example (example at line 160) line 160 source
  31. example (example at line 174) line 174 source