1. Top
  2. mathematics_in_lean
  3. Files
  4. html
  5. C09_Topology.html
mathematics_in_lean

My solutions for this book

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24
  25. 25
  26. 26
  27. 27
  28. 28
  29. 29
  30. 30
  31. 31
  32. 32
  33. 33
  34. 34
  35. 35
  36. 36
  37. 37
  38. 38
  39. 39
  40. 40
  41. 41
  42. 42
  43. 43
  44. 44
  45. 45
  46. 46
  47. 47
  48. 48
  49. 49
  50. 50
  51. 51
  52. 52
  53. 53
  54. 54
  55. 55
  56. 56
  57. 57
  58. 58
  59. 59
  60. 60
  61. 61
  62. 62
  63. 63
  64. 64
  65. 65
  66. 66
  67. 67
  68. 68
  69. 69
  70. 70
  71. 71
  72. 72
  73. 73
  74. 74
  75. 75
  76. 76
  77. 77
  78. 78
  79. 79
  80. 80
  81. 81
  82. 82
  83. 83
  84. 84
  85. 85
  86. 86
  87. 87
  88. 88
  89. 89
  90. 90
  91. 91
  92. 92
  93. 93
  94. 94
  95. 95
  96. 96
  97. 97
  98. 98
  99. 99
  100. 100
  101. 101
  102. 102
  103. 103
  104. 104
  105. 105
  106. 106
  107. 107
  108. 108
  109. 109
  110. 110
  111. 111
  112. 112
  113. 113
  114. 114
  115. 115
  116. 116
  117. 117
  118. 118
  119. 119
  120. 120
  121. 121
  122. 122
  123. 123
  124. 124
  125. 125
  126. 126
  127. 127
  128. 128
  129. 129
  130. 130
  131. 131
  132. 132
  133. 133
  134. 134
  135. 135
  136. 136
  137. 137
  138. 138
  139. 139
  140. 140
  141. 141
  142. 142
  143. 143
  144. 144
  145. 145
  146. 146
  147. 147
  148. 148
  149. 149
  150. 150
  151. 151
  152. 152
  153. 153
  154. 154
  155. 155
  156. 156
  157. 157
  158. 158
  159. 159
  160. 160
  161. 161
  162. 162
  163. 163
  164. 164
  165. 165
  166. 166
  167. 167
  168. 168
  169. 169
  170. 170
  171. 171
  172. 172
  173. 173
  174. 174
  175. 175
  176. 176
  177. 177
  178. 178
  179. 179
  180. 180
  181. 181
  182. 182
  183. 183
  184. 184
  185. 185
  186. 186
  187. 187
  188. 188
  189. 189
  190. 190
  191. 191
  192. 192
  193. 193
  194. 194
  195. 195
  196. 196
  197. 197
  198. 198
  199. 199
  200. 200
  201. 201
  202. 202
  203. 203
  204. 204
  205. 205
  206. 206
  207. 207
  208. 208
  209. 209
  210. 210
  211. 211
  212. 212
  213. 213
  214. 214
  215. 215
  216. 216
  217. 217
  218. 218
  219. 219
  220. 220
  221. 221
  222. 222
  223. 223
  224. 224
  225. 225
  226. 226
  227. 227
  228. 228
  229. 229
  230. 230
  231. 231
  232. 232
  233. 233
  234. 234
  235. 235
  236. 236
  237. 237
  238. 238
  239. 239
  240. 240
  241. 241
  242. 242
  243. 243
  244. 244
  245. 245
  246. 246
  247. 247
  248. 248
  249. 249
  250. 250
  251. 251
  252. 252
  253. 253
  254. 254
  255. 255
  256. 256
  257. 257
  258. 258
  259. 259
  260. 260
  261. 261
  262. 262
  263. 263
  264. 264
  265. 265
  266. 266
  267. 267
  268. 268
  269. 269
  270. 270
  271. 271
  272. 272
  273. 273
  274. 274
  275. 275
  276. 276
  277. 277
  278. 278
  279. 279
  280. 280
  281. 281
  282. 282
  283. 283
  284. 284
  285. 285
  286. 286
  287. 287
  288. 288
  289. 289
  290. 290
  291. 291
  292. 292
  293. 293
  294. 294
  295. 295
  296. 296
  297. 297
  298. 298
  299. 299
  300. 300
  301. 301
  302. 302
  303. 303
  304. 304
  305. 305
  306. 306
  307. 307
  308. 308
  309. 309
  310. 310
  311. 311
  312. 312
  313. 313
  314. 314
  315. 315
  316. 316
  317. 317
  318. 318
  319. 319
  320. 320
  321. 321
  322. 322
  323. 323
  324. 324
  325. 325
  326. 326
  327. 327
  328. 328
  329. 329
  330. 330
  331. 331
  332. 332
  333. 333
  334. 334
  335. 335
  336. 336
  337. 337
  338. 338
  339. 339
  340. 340
  341. 341
  342. 342
  343. 343
  344. 344
  345. 345
  346. 346
  347. 347
  348. 348
  349. 349
  350. 350
  351. 351
  352. 352
  353. 353
  354. 354
  355. 355
  356. 356
  357. 357
  358. 358
  359. 359
  360. 360
  361. 361
  362. 362
  363. 363
  364. 364
  365. 365
  366. 366
  367. 367
  368. 368
  369. 369
  370. 370
  371. 371
  372. 372
  373. 373
  374. 374
  375. 375
  376. 376
  377. 377
  378. 378
  379. 379
  380. 380
  381. 381
  382. 382
  383. 383
  384. 384
  385. 385
  386. 386
  387. 387
  388. 388
  389. 389
  390. 390
  391. 391
  392. 392
  393. 393
  394. 394
  395. 395
  396. 396
  397. 397
  398. 398
  399. 399
  400. 400
  401. 401
  402. 402
  403. 403
  404. 404
  405. 405
  406. 406
  407. 407
  408. 408
  409. 409
  410. 410
  411. 411
  412. 412
  413. 413
  414. 414
  415. 415
  416. 416
  417. 417
  418. 418
  419. 419
  420. 420
  421. 421
  422. 422
  423. 423
  424. 424
  425. 425
  426. 426
  427. 427
  428. 428
  429. 429
  430. 430
  431. 431
  432. 432
  433. 433
  434. 434
  435. 435
  436. 436
  437. 437
  438. 438
  439. 439
  440. 440
  441. 441
  442. 442
  443. 443
  444. 444
  445. 445
  446. 446
  447. 447
  448. 448
  449. 449
  450. 450
  451. 451
  452. 452
  453. 453
  454. 454
  455. 455
  456. 456
  457. 457
  458. 458
  459. 459
  460. 460
  461. 461
  462. 462
  463. 463
  464. 464
  465. 465
  466. 466
  467. 467
  468. 468
  469. 469
  470. 470
  471. 471
  472. 472
  473. 473
  474. 474
  475. 475
  476. 476
  477. 477
  478. 478
  479. 479
  480. 480
  481. 481
  482. 482
  483. 483
  484. 484
  485. 485
  486. 486
  487. 487
  488. 488
  489. 489
  490. 490
  491. 491
  492. 492
  493. 493
  494. 494
  495. 495
  496. 496
  497. 497
  498. 498
  499. 499
  500. 500
  501. 501
  502. 502
  503. 503
  504. 504
  505. 505
  506. 506
  507. 507
  508. 508
  509. 509
  510. 510
  511. 511
  512. 512
  513. 513
  514. 514
  515. 515
  516. 516
  517. 517
  518. 518
  519. 519
  520. 520
  521. 521
  522. 522
  523. 523
  524. 524
  525. 525
  526. 526
  527. 527
  528. 528
  529. 529
  530. 530
  531. 531
  532. 532
  533. 533
  534. 534
  535. 535
  536. 536
  537. 537
  538. 538
  539. 539
  540. 540
  541. 541
  542. 542
  543. 543
  544. 544
  545. 545
  546. 546
  547. 547
  548. 548
  549. 549
  550. 550
  551. 551
  552. 552
  553. 553
  554. 554
  555. 555
  556. 556
  557. 557
  558. 558
  559. 559
  560. 560
  561. 561
  562. 562
  563. 563
  564. 564
  565. 565
  566. 566
  567. 567
  568. 568
  569. 569
  570. 570
  571. 571
  572. 572
  573. 573
  574. 574
  575. 575
  576. 576
  577. 577
  578. 578
  579. 579
  580. 580
  581. 581
  582. 582
  583. 583
  584. 584
  585. 585
  586. 586
  587. 587
  588. 588
  589. 589
  590. 590
  591. 591
  592. 592
  593. 593
  594. 594
  595. 595
  596. 596
  597. 597
  598. 598
  599. 599
  600. 600
  601. 601
  602. 602
  603. 603
  604. 604
  605. 605
  606. 606
  607. 607
  608. 608
  609. 609
  610. 610
  611. 611
  612. 612
  613. 613
  614. 614
  615. 615
  616. 616
  617. 617
  618. 618
  619. 619
  620. 620
  621. 621
  622. 622
  623. 623
  624. 624
  625. 625
  626. 626
  627. 627
  628. 628
  629. 629
  630. 630
  631. 631
  632. 632
  633. 633
  634. 634
  635. 635
  636. 636
  637. 637
  638. 638
  639. 639
  640. 640
  641. 641
  642. 642
  643. 643
  644. 644
  645. 645
  646. 646
  647. 647
  648. 648
  649. 649
  650. 650
  651. 651
  652. 652
  653. 653
  654. 654
  655. 655
  656. 656
  657. 657
  658. 658
  659. 659
  660. 660
  661. 661
  662. 662
  663. 663
  664. 664
  665. 665
  666. 666
  667. 667
  668. 668
  669. 669
  670. 670
  671. 671
  672. 672
  673. 673
  674. 674
  675. 675
  676. 676
  677. 677
  678. 678
  679. 679
  680. 680
  681. 681
  682. 682
  683. 683
  684. 684
  685. 685
  686. 686
  687. 687
  688. 688
  689. 689
  690. 690
  691. 691
  692. 692
  693. 693
  694. 694
  695. 695
  696. 696
  697. 697
  698. 698
  699. 699
  700. 700
  701. 701
  702. 702
  703. 703
  704. 704
  705. 705
  706. 706
  707. 707
  708. 708
  709. 709
  710. 710
  711. 711
  712. 712
  713. 713
  714. 714
  715. 715
  716. 716
  717. 717
  718. 718
  719. 719
  720. 720
  721. 721
  722. 722
  723. 723
  724. 724
  725. 725
  726. 726
  727. 727
  728. 728
  729. 729
  730. 730
  731. 731
  732. 732
  733. 733
  734. 734
  735. 735
  736. 736
  737. 737
  738. 738
  739. 739
  740. 740
  741. 741
  742. 742
  743. 743
  744. 744
  745. 745
  746. 746
  747. 747
  748. 748
  749. 749
  750. 750
  751. 751
  752. 752
  753. 753
  754. 754
  755. 755
  756. 756
  757. 757
  758. 758
  759. 759
  760. 760
  761. 761
  762. 762
  763. 763
  764. 764
  765. 765
  766. 766
  767. 767
  768. 768
  769. 769
  770. 770
  771. 771
  772. 772
  773. 773
  774. 774
  775. 775
  776. 776
  777. 777
  778. 778
  779. 779
  780. 780
  781. 781
  782. 782
  783. 783
  784. 784
  785. 785
  786. 786
  787. 787
  788. 788
  789. 789
  790. 790
  791. 791
  792. 792
  793. 793
  794. 794
  795. 795
  796. 796
  797. 797
  798. 798
  799. 799
  800. 800
  801. 801
  802. 802
  803. 803
  804. 804
  805. 805
  806. 806
  807. 807
  808. 808
  809. 809
  810. 810
  811. 811
  812. 812
  813. 813
  814. 814
  815. 815
  816. 816
  817. 817
  818. 818
  819. 819
  820. 820
  821. 821
  822. 822
  823. 823
  824. 824
  825. 825
  826. 826
  827. 827
  828. 828
  829. 829
  830. 830
  831. 831
  832. 832
  833. 833
  834. 834
  835. 835
  836. 836
  837. 837
  838. 838
  839. 839
  840. 840
  841. 841
  842. 842
  843. 843
  844. 844
  845. 845
  846. 846
  847. 847
  848. 848
  849. 849
  850. 850
  851. 851
  852. 852
  853. 853
  854. 854
  855. 855
  856. 856
  857. 857
  858. 858
  859. 859
  860. 860
  861. 861
  862. 862
  863. 863
  864. 864
  865. 865
  866. 866
  867. 867
  868. 868
  869. 869
  870. 870
  871. 871
  872. 872
  873. 873
  874. 874
  875. 875
  876. 876
  877. 877
  878. 878
  879. 879
  880. 880
  881. 881
  882. 882
  883. 883
  884. 884
  885. 885
  886. 886
  887. 887
  888. 888
  889. 889
  890. 890
  891. 891
  892. 892
  893. 893
  894. 894
  895. 895
  896. 896
  897. 897
  898. 898
  899. 899
  900. 900
  901. 901
  902. 902
  903. 903
  904. 904
  905. 905
  906. 906
  907. 907
  908. 908
  909. 909
  910. 910
  911. 911
  912. 912
  913. 913
  914. 914
  915. 915
  916. 916
  917. 917
  918. 918
  919. 919
  920. 920
  921. 921
  922. 922
  923. 923
  924. 924
  925. 925
  926. 926
  927. 927
  928. 928
  929. 929
  930. 930
  931. 931
  932. 932
  933. 933
  934. 934
  935. 935
  936. 936
  937. 937
  938. 938
  939. 939
  940. 940
  941. 941
  942. 942
  943. 943
  944. 944
  945. 945
  946. 946
  947. 947
  948. 948
  949. 949
  950. 950
  951. 951
  952. 952
  953. 953
  954. 954
  955. 955
  956. 956
  957. 957
  958. 958
  959. 959
  960. 960
  961. 961
  962. 962
  963. 963
  964. 964
  965. 965
  966. 966
  967. 967
  968. 968
  969. 969
  970. 970
  971. 971
  972. 972
  973. 973
  974. 974
  975. 975
  976. 976
  977. 977
  978. 978
  979. 979
  980. 980
  981. 981
  982. 982
  983. 983
  984. 984
  985. 985
  986. 986
  987. 987
  988. 988
  989. 989
  990. 990
  991. 991
  992. 992
  993. 993
  994. 994
  995. 995
  996. 996
  997. 997
  998. 998
  999. 999
  1000. 1000
  1001. 1001
  1002. 1002
  1003. 1003
  1004. 1004
  1005. 1005
  1006. 1006
  1007. 1007
  1008. 1008
  1009. 1009
  1010. 1010
  1011. 1011
  1012. 1012
  1013. 1013
  1014. 1014
  1015. 1015
  1016. 1016
  1017. 1017
  1018. 1018
  1019. 1019
  1020. 1020
  1021. 1021
  1022. 1022
  1023. 1023
  1024. 1024
  1025. 1025
  1026. 1026
  1027. 1027
  1028. 1028
  1029. 1029
  1030. 1030
  1031. 1031
  1032. 1032
  1033. 1033
  1034. 1034
  1035. 1035
  1036. 1036
  1037. 1037
  1038. 1038
  1039. 1039
  1040. 1040
  1041. 1041
  1042. 1042
  1043. 1043
  1044. 1044
  1045. 1045
  1046. 1046
  1047. 1047
  1048. 1048
  1049. 1049
  1050. 1050
  1051. 1051
  1052. 1052
  1053. 1053
  1054. 1054
  1055. 1055
  1056. 1056
  1057. 1057
  1058. 1058
  1059. 1059
  1060. 1060
  1061. 1061
  1062. 1062
  1063. 1063
  1064. 1064
  1065. 1065
  1066. 1066
  1067. 1067
  1068. 1068
  1069. 1069
  1070. 1070
  1071. 1071
  1072. 1072
  1073. 1073
  1074. 1074
  1075. 1075
  1076. 1076
  1077. 1077
  1078. 1078
  1079. 1079
  1080. 1080
  1081. 1081
  1082. 1082
  1083. 1083
  1084. 1084
  1085. 1085
  1086. 1086
  1087. 1087
  1088. 1088
  1089. 1089
  1090. 1090
  1091. 1091
  1092. 1092
  1093. 1093
  1094. 1094
  1095. 1095
  1096. 1096
  1097. 1097
  1098. 1098
  1099. 1099
  1100. 1100
  1101. 1101
  1102. 1102
  1103. 1103
  1104. 1104
  1105. 1105
  1106. 1106
  1107. 1107
  1108. 1108
  1109. 1109
  1110. 1110
  1111. 1111
  1112. 1112
  1113. 1113
  1114. 1114
  1115. 1115
  1116. 1116
  1117. 1117
  1118. 1118
  1119. 1119
  1120. 1120
  1121. 1121
  1122. 1122
  1123. 1123
  1124. 1124
  1125. 1125
  1126. 1126
  1127. 1127
  1128. 1128
  1129. 1129
  1130. 1130
  1131. 1131
  1132. 1132
  1133. 1133
  1134. 1134
  1135. 1135
  1136. 1136
  1137. 1137
  1138. 1138
  1139. 1139
  1140. 1140
  1141. 1141
  1142. 1142
  1143. 1143
  1144. 1144
  1145. 1145
  1146. 1146
  1147. 1147
  1148. 1148
  1149. 1149
  1150. 1150
  1151. 1151
  1152. 1152
  1153. 1153
  1154. 1154
  1155. 1155
  1156. 1156
  1157. 1157
  1158. 1158
  1159. 1159
  1160. 1160
  1161. 1161
  1162. 1162
  1163. 1163
  1164. 1164
  1165. 1165
  1166. 1166
  1167. 1167
  1168. 1168
  1169. 1169
  1170. 1170
  1171. 1171
  1172. 1172
  1173. 1173
  1174. 1174
  1175. 1175
  1176. 1176
  1177. 1177
  1178. 1178
  1179. 1179
  1180. 1180
  1181. 1181
  1182. 1182
  1183. 1183
  1184. 1184
  1185. 1185
  1186. 1186
  1187. 1187
  1188. 1188
  1189. 1189
  1190. 1190
  1191. 1191
  1192. 1192
  1193. 1193
  1194. 1194
  1195. 1195
  1196. 1196
  1197. 1197
  1198. 1198
  1199. 1199
  1200. 1200
  1201. 1201
  1202. 1202
  1203. 1203
  1204. 1204
  1205. 1205
  1206. 1206
  1207. 1207
  1208. 1208
  1209. 1209
  1210. 1210
  1211. 1211
  1212. 1212
  1213. 1213
  1214. 1214
  1215. 1215
  1216. 1216
  1217. 1217
  1218. 1218
  1219. 1219
  1220. 1220
  1221. 1221
  1222. 1222
  1223. 1223
  1224. 1224
  1225. 1225
  1226. 1226
  1227. 1227 
<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>9. Topology &mdash; Mathematics in Lean 0.1 documentation</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
        <script src="_static/doctools.js"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="10. Differential Calculus" href="C10_Differential_Calculus.html" />
    <link rel="prev" title="8. Groups and Rings" href="C08_Groups_and_Rings.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >
            <a href="index.html" class="icon icon-home"> Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Structures.html">6. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Hierarchies.html">7. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Groups_and_Rings.html">8. Groups and Rings</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">9. Topology</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#filters">9.1. Filters</a></li>
<li class="toctree-l2"><a class="reference internal" href="#metric-spaces">9.2. Metric spaces</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#convergence-and-continuity">9.2.1. Convergence and continuity</a></li>
<li class="toctree-l3"><a class="reference internal" href="#balls-open-sets-and-closed-sets">9.2.2. Balls, open sets and closed sets</a></li>
<li class="toctree-l3"><a class="reference internal" href="#compactness">9.2.3. Compactness</a></li>
<li class="toctree-l3"><a class="reference internal" href="#uniformly-continuous-functions">9.2.4. Uniformly continuous functions</a></li>
<li class="toctree-l3"><a class="reference internal" href="#completeness">9.2.5. Completeness</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#topological-spaces">9.3. Topological spaces</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#fundamentals">9.3.1. Fundamentals</a></li>
<li class="toctree-l3"><a class="reference internal" href="#separation-and-countability">9.3.2. Separation and countability</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id5">9.3.3. Compactness</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C10_Differential_Calculus.html">10. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Integration_and_Measure_Theory.html">11. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
      <li><span class="section-number">9. </span>Topology</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C09_Topology.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <span class="target" id="topology"></span><section id="index-0">
<span id="id1"></span><h1><span class="section-number">9. </span>Topology<a class="headerlink" href="#index-0" title="Permalink to this heading">&#61633;</a></h1>
<p>Calculus is based on the concept of a function, which is used to model
quantities that depend on one another.
For example, it is common to study quantities that change over time.
The notion of a <em>limit</em> is also fundamental.
We may say that the limit of a function <span class="math notranslate nohighlight">\(f(x)\)</span> is a value <span class="math notranslate nohighlight">\(b\)</span>
as <span class="math notranslate nohighlight">\(x\)</span> approaches a value <span class="math notranslate nohighlight">\(a\)</span>,
or that <span class="math notranslate nohighlight">\(f(x)\)</span> <em>converges to</em> <span class="math notranslate nohighlight">\(b\)</span> as <span class="math notranslate nohighlight">\(x\)</span> approaches <span class="math notranslate nohighlight">\(a\)</span>.
Equivalently, we may say that a <span class="math notranslate nohighlight">\(f(x)\)</span> approaches <span class="math notranslate nohighlight">\(a\)</span> as <span class="math notranslate nohighlight">\(x\)</span>
approaches a value <span class="math notranslate nohighlight">\(b\)</span>, or that it <em>tends to</em> <span class="math notranslate nohighlight">\(b\)</span>
as <span class="math notranslate nohighlight">\(x\)</span> tends to <span class="math notranslate nohighlight">\(a\)</span>.
We have already begun to consider such notions in <a class="reference internal" href="C03_Logic.html#sequences-and-convergence"><span class="std std-numref">Section 3.6</span></a>.</p>
<p><em>Topology</em> is the abstract study of limits and continuity.
Having covered the essentials of formalization in Chapters <a class="reference internal" href="C02_Basics.html#basics"><span class="std std-numref">2</span></a>
to <a class="reference internal" href="C06_Structures.html#structures"><span class="std std-numref">6</span></a>,
in this chapter, we will explain how topological notions are formalized in Mathlib.
Not only do topological abstractions apply in much greater generality,
but that also, somewhat paradoxically, make it easier to reason about limits
and continuity in concrete instances.</p>
<p>Topological notions build on quite a few layers of mathematical structure.
The first layer is naive set theory,
as described in <a class="reference internal" href="C04_Sets_and_Functions.html#sets-and-functions"><span class="std std-numref">Chapter 4</span></a>.
The next layer is the theory of <em>filters</em>, which we will describe in <a class="reference internal" href="#filters"><span class="std std-numref">Section 9.1</span></a>.
On top of that, we layer
the theories of <em>topological spaces</em>, <em>metric spaces</em>, and a slightly more exotic
intermediate notion called a <em>uniform space</em>.</p>
<p>Whereas previous chapters relied on mathematical notions that were likely
familiar to you,
the notion of a filter less well known,
even to many working mathematicians.
The notion is essential, however, for formalizing mathematics effectively.
Let us explain why.
Let <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> be any function. We can consider
the limit of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> as <code class="docutils literal notranslate"><span class="pre">x</span></code> approaches some value <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code>,
but we can also consider the limit of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> as <code class="docutils literal notranslate"><span class="pre">x</span></code> approaches infinity
or negative infinity.
We can moreover consider the limit of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> as <code class="docutils literal notranslate"><span class="pre">x</span></code> approaches <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> from
the right, conventionally written <code class="docutils literal notranslate"><span class="pre">x&#8320;&#8314;</span></code>, or from the left,
written  <code class="docutils literal notranslate"><span class="pre">x&#8320;&#8315;</span></code>. There are variations where <code class="docutils literal notranslate"><span class="pre">x</span></code> approaches <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> or <code class="docutils literal notranslate"><span class="pre">x&#8320;&#8314;</span></code>
or <code class="docutils literal notranslate"><span class="pre">x&#8320;&#8315;</span></code> but
is not allowed to take on the value <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> itself.
This results in at least eight ways that <code class="docutils literal notranslate"><span class="pre">x</span></code> can approach something.
We can also restrict to rational values of <code class="docutils literal notranslate"><span class="pre">x</span></code>
or place other constraints on the domain, but let&#8217;s stick to those 8 cases.</p>
<p>We have a similar variety of options on the codomain:
we can specify that <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> approaches a value from the left or right,
or that it approaches positive or negative infinity, and so on.
For example, we may wish to say that <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> tends to <code class="docutils literal notranslate"><span class="pre">+&#8734;</span></code>
when <code class="docutils literal notranslate"><span class="pre">x</span></code> tends to <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> from the right without
being equal to <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code>.
This results in 64 different kinds of limit statements,
and we haven&#8217;t even begun to deal with limits of sequences,
as we did in <a class="reference internal" href="C03_Logic.html#sequences-and-convergence"><span class="std std-numref">Section 3.6</span></a>.</p>
<p>The problem is compounded even further when it comes to the supporting lemmas.
For instance, limits compose: if
<code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> tends to <code class="docutils literal notranslate"><span class="pre">y&#8320;</span></code> when <code class="docutils literal notranslate"><span class="pre">x</span></code> tends to <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> and
<code class="docutils literal notranslate"><span class="pre">g</span> <span class="pre">y</span></code> tends to <code class="docutils literal notranslate"><span class="pre">z&#8320;</span></code> when <code class="docutils literal notranslate"><span class="pre">y</span></code> tends to <code class="docutils literal notranslate"><span class="pre">y&#8320;</span></code> then
<code class="docutils literal notranslate"><span class="pre">g</span> <span class="pre">&#8728;</span> <span class="pre">f</span> <span class="pre">x</span></code> tends to <code class="docutils literal notranslate"><span class="pre">z&#8320;</span></code> when <code class="docutils literal notranslate"><span class="pre">x</span></code> tends to <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code>.
There are three notions of &#8220;tends to&#8221; at play here,
each of which can be instantiated in any of the eight ways described
in the previous paragraph.
This results in 512 lemmas, a lot to have to add to a library!
Informally, mathematicians generally prove two or three of these
and simply note that the rest can be proved &#8220;in the same way.&#8221;
Formalizing mathematics requires making the relevant notion of &#8220;sameness&#8221;
fully explicit, and that is exactly what Bourbaki&#8217;s theory of filters
manages to do.</p>
<section id="filters">
<span id="index-1"></span><span id="id2"></span><h2><span class="section-number">9.1. </span>Filters<a class="headerlink" href="#filters" title="Permalink to this heading">&#61633;</a></h2>
<p>A <em>filter</em> on a type <code class="docutils literal notranslate"><span class="pre">X</span></code> is a collection of sets of <code class="docutils literal notranslate"><span class="pre">X</span></code> that satisfies three
conditions that we will spell out below. The notion
supports two related ideas:</p>
<ul class="simple">
<li><p><em>limits</em>, including all the kinds of limits discussed above: finite and infinite limits of sequences, finite and infinite limits of functions at a point or at infinity, and so on.</p></li>
<li><p><em>things happening eventually</em>, including things happening for large enough <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">:</span> <span class="pre">&#8469;</span></code>, or sufficiently near a point <code class="docutils literal notranslate"><span class="pre">x</span></code>, or for sufficiently close pairs of points, or almost everywhere in the sense of measure theory. Dually, filters can also express the idea of <em>things happening often</em>: for arbitrarily large <code class="docutils literal notranslate"><span class="pre">n</span></code>, at a point in any neighborhood of given a point, etc.</p></li>
</ul>
<p>The filters that correspond to these descriptions will be defined later in this section, but we can already name them:</p>
<ul class="simple">
<li><p><code class="docutils literal notranslate"><span class="pre">(atTop</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">&#8469;)</span></code>, made of sets of <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> containing <code class="docutils literal notranslate"><span class="pre">{n</span> <span class="pre">|</span> <span class="pre">n</span> <span class="pre">&#8805;</span> <span class="pre">N}</span></code> for some <code class="docutils literal notranslate"><span class="pre">N</span></code></p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x</span></code>, made of neighborhoods of <code class="docutils literal notranslate"><span class="pre">x</span></code> in a topological space</p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">&#120036;</span> <span class="pre">X</span></code>, made of entourages of a uniform space (uniform spaces generalize metric spaces and topological groups)</p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">&#956;.ae</span></code> , made of sets whose complement has zero measure with respect to a measure <code class="docutils literal notranslate"><span class="pre">&#956;</span></code>.</p></li>
</ul>
<p>The general definition is as follows: a filter <code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">X</span></code> is a
collection of sets <code class="docutils literal notranslate"><span class="pre">F.sets</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">(Set</span> <span class="pre">X)</span></code> satisfying the following:</p>
<ul class="simple">
<li><p><code class="docutils literal notranslate"><span class="pre">F.univ_sets</span> <span class="pre">:</span> <span class="pre">univ</span> <span class="pre">&#8712;</span> <span class="pre">F.sets</span></code></p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">F.sets_of_superset</span> <span class="pre">:</span> <span class="pre">&#8704;</span> <span class="pre">{U</span> <span class="pre">V},</span> <span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F.sets</span> <span class="pre">&#8594;</span> <span class="pre">U</span> <span class="pre">&#8838;</span> <span class="pre">V</span> <span class="pre">&#8594;</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">F.sets</span></code></p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">F.inter_sets</span> <span class="pre">:</span> <span class="pre">&#8704;</span> <span class="pre">{U</span> <span class="pre">V},</span> <span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F.sets</span> <span class="pre">&#8594;</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">F.sets</span> <span class="pre">&#8594;</span> <span class="pre">U</span> <span class="pre">&#8745;</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">F.sets</span></code>.</p></li>
</ul>
<p>The first condition says that the set of all elements of <code class="docutils literal notranslate"><span class="pre">X</span></code> belongs to <code class="docutils literal notranslate"><span class="pre">F.sets</span></code>.
The second condition says that if <code class="docutils literal notranslate"><span class="pre">U</span></code> belongs to <code class="docutils literal notranslate"><span class="pre">F.sets</span></code> then anything
containing <code class="docutils literal notranslate"><span class="pre">U</span></code> also belongs to <code class="docutils literal notranslate"><span class="pre">F.sets</span></code>.
The third condition says that <code class="docutils literal notranslate"><span class="pre">F.sets</span></code> is closed under finite intersections.
In Mathlib, a filter <code class="docutils literal notranslate"><span class="pre">F</span></code> is defined to be a structure bundling <code class="docutils literal notranslate"><span class="pre">F.sets</span></code> and its
three properties, but the properties carry no additional data,
and it is convenient to blur the distinction between <code class="docutils literal notranslate"><span class="pre">F</span></code> and <code class="docutils literal notranslate"><span class="pre">F.sets</span></code>. We
therefore define <code class="docutils literal notranslate"><span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code> to mean <code class="docutils literal notranslate"><span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F.sets</span></code>.
This explains why the word <code class="docutils literal notranslate"><span class="pre">sets</span></code> appears in the names of some lemmas that
that mention <code class="docutils literal notranslate"><span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code>.</p>
<p>It may help to think of a filter as defining a notion of a &#8220;sufficiently large&#8221; set. The first
condition then says that <code class="docutils literal notranslate"><span class="pre">univ</span></code> is sufficiently large, the second one says that a set containing a sufficiently
large set is sufficiently large and the third one says that the intersection of two sufficiently large sets
is sufficiently large.</p>
<p>It may be even  more useful to think of a filter on a type <code class="docutils literal notranslate"><span class="pre">X</span></code>
as a generalized element of <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">X</span></code>. For instance, <code class="docutils literal notranslate"><span class="pre">atTop</span></code> is the
&#8220;set of very large numbers&#8221; and <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x&#8320;</span></code> is the &#8220;set of points very close to <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code>.&#8221;
One manifestation of this view is that we can associate to any <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">X</span></code> the so-called <em>principal filter</em>
consisting of all sets that contain <code class="docutils literal notranslate"><span class="pre">s</span></code>.
This definition is already in Mathlib and has a notation <code class="docutils literal notranslate"><span class="pre">&#120031;</span></code> (localized in the <code class="docutils literal notranslate"><span class="pre">Filter</span></code> namespace).
For the purpose of demonstration, we ask you to take this opportunity to work out the definition here.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">principal</span> <span class="o">{</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">(</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">&#945;</span>
    <span class="n">where</span>
  <span class="n">sets</span> <span class="o">:=</span> <span class="o">{</span> <span class="n">t</span> <span class="bp">|</span> <span class="n">s</span> <span class="bp">&#8838;</span> <span class="n">t</span> <span class="o">}</span>
  <span class="n">univ_sets</span> <span class="o">:=</span> <span class="gr">sorry</span>
  <span class="n">sets_of_superset</span> <span class="o">:=</span> <span class="gr">sorry</span>
  <span class="n">inter_sets</span> <span class="o">:=</span> <span class="gr">sorry</span>
</pre></div>
</div>
<p>For our second example, we ask you to define the filter <code class="docutils literal notranslate"><span class="pre">atTop</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">&#8469;</span></code>.
(We could use any type with a preorder instead of <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code>.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">&#8469;</span> <span class="o">:=</span>
  <span class="o">{</span> <span class="n">sets</span> <span class="o">:=</span> <span class="o">{</span> <span class="n">s</span> <span class="bp">|</span> <span class="bp">&#8707;</span> <span class="n">a</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">b</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">b</span> <span class="bp">&#8594;</span> <span class="n">b</span> <span class="bp">&#8712;</span> <span class="n">s</span> <span class="o">}</span>
    <span class="n">univ_sets</span> <span class="o">:=</span> <span class="gr">sorry</span>
    <span class="n">sets_of_superset</span> <span class="o">:=</span> <span class="gr">sorry</span>
    <span class="n">inter_sets</span> <span class="o">:=</span> <span class="gr">sorry</span> <span class="o">}</span>
</pre></div>
</div>
<p>We can also directly define the filter <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x</span></code> of neighborhoods of any <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">:</span> <span class="pre">&#8477;</span></code>.
In the real numbers, a neighborhood of <code class="docutils literal notranslate"><span class="pre">x</span></code> is a set containing an open interval
<span class="math notranslate nohighlight">\((x_0 - \varepsilon, x_0 + \varepsilon)\)</span>,
defined in Mathlib as <code class="docutils literal notranslate"><span class="pre">Ioo</span> <span class="pre">(x&#8320;</span> <span class="pre">-</span> <span class="pre">&#949;)</span> <span class="pre">(x&#8320;</span> <span class="pre">+</span> <span class="pre">&#949;)</span></code>.
(This is notion of a neighborhood is only a special case of a more general construction in Mathlib.)</p>
<p>With these examples, we can already define what is means for a function <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Y</span></code>
to converge to some <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">Y</span></code> along some <code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">X</span></code>,
as follows:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Tendsto&#8321;</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">G</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:=</span>
  <span class="bp">&#8704;</span> <span class="n">V</span> <span class="bp">&#8712;</span> <span class="n">G</span><span class="o">,</span> <span class="n">f</span> <span class="bp">&#8315;&#185;&#39;</span> <span class="n">V</span> <span class="bp">&#8712;</span> <span class="n">F</span>
</pre></div>
</div>
<p>When <code class="docutils literal notranslate"><span class="pre">X</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> and <code class="docutils literal notranslate"><span class="pre">Y</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>, <code class="docutils literal notranslate"><span class="pre">Tendsto&#8321;</span> <span class="pre">u</span> <span class="pre">atTop</span> <span class="pre">(&#120029;</span> <span class="pre">x)</span></code> is equivalent to saying that the sequence <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">:</span> <span class="pre">&#8469;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code>
converges to the real number <code class="docutils literal notranslate"><span class="pre">x</span></code>. When both <code class="docutils literal notranslate"><span class="pre">X</span></code> and <code class="docutils literal notranslate"><span class="pre">Y</span></code> are <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>, <code class="docutils literal notranslate"><span class="pre">Tendsto</span> <span class="pre">f</span> <span class="pre">(&#120029;</span> <span class="pre">x&#8320;)</span> <span class="pre">(&#120029;</span> <span class="pre">y&#8320;)</span></code>
is equivalent to the familiar notion <span class="math notranslate nohighlight">\(\lim_{x \to x&#8320;} f(x) = y&#8320;\)</span>.
All of the other kinds of limits mentioned in the introduction are
also equivalent to instances of <code class="docutils literal notranslate"><span class="pre">Tendsto&#8321;</span></code> for suitable choices of filters on the source and target.</p>
<p>The notion <code class="docutils literal notranslate"><span class="pre">Tendsto&#8321;</span></code> above is definitionally equivalent to the notion <code class="docutils literal notranslate"><span class="pre">Tendsto</span></code> that is defined in Mathlib,
but the latter is defined more abstractly.
The problem with the definition of <code class="docutils literal notranslate"><span class="pre">Tendsto&#8321;</span></code> is that it exposes a quantifier and elements of <code class="docutils literal notranslate"><span class="pre">G</span></code>,
and it hides the intuition that we get by viewing filters as generalized sets. We can
hide the quantifier <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">V</span></code> and make the intuition more salient by using more algebraic and set-theoretic machinery.
The first ingredient is the <em>pushforward</em> operation <span class="math notranslate nohighlight">\(f_*\)</span> associated to any map <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Y</span></code>,
denoted <code class="docutils literal notranslate"><span class="pre">Filter.map</span> <span class="pre">f</span></code> in Mathlib. Given a filter <code class="docutils literal notranslate"><span class="pre">F</span></code> on <code class="docutils literal notranslate"><span class="pre">X</span></code>, <code class="docutils literal notranslate"><span class="pre">Filter.map</span> <span class="pre">f</span> <span class="pre">F</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">Y</span></code> is defined so that
<code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">Filter.map</span> <span class="pre">f</span> <span class="pre">F</span> <span class="pre">&#8596;</span> <span class="pre">f</span> <span class="pre">&#8315;&#185;'</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code> holds definitionally.
In this examples file we&#8217;ve opened the <code class="docutils literal notranslate"><span class="pre">Filter</span></code> namespace so that
<code class="docutils literal notranslate"><span class="pre">Filter.map</span></code> can be written as <code class="docutils literal notranslate"><span class="pre">map</span></code>. This means that we can rewrite the definition of <code class="docutils literal notranslate"><span class="pre">Tendsto</span></code> using
the order relation on <code class="docutils literal notranslate"><span class="pre">Filter</span> <span class="pre">Y</span></code>, which is reversed inclusion of the set of members.
In other words, given <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">H</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">Y</span></code>, we have <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#8804;</span> <span class="pre">H</span> <span class="pre">&#8596;</span> <span class="pre">&#8704;</span> <span class="pre">V</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">Y,</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">H</span> <span class="pre">&#8594;</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">G</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Tendsto&#8322;</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">G</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">map</span> <span class="n">f</span> <span class="n">F</span> <span class="bp">&#8804;</span> <span class="n">G</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">G</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Tendsto&#8322;</span> <span class="n">f</span> <span class="n">F</span> <span class="n">G</span> <span class="bp">&#8596;</span> <span class="n">Tendsto&#8321;</span> <span class="n">f</span> <span class="n">F</span> <span class="n">G</span> <span class="o">:=</span>
  <span class="n">Iff.rfl</span>
</pre></div>
</div>
<p>It may seem that the order relation on filters is backward. But recall that we can view filters on <code class="docutils literal notranslate"><span class="pre">X</span></code> as
generalized elements of <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">X</span></code>, via the inclusion of <code class="docutils literal notranslate"><span class="pre">&#120031;</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">X</span></code> which maps any set <code class="docutils literal notranslate"><span class="pre">s</span></code> to the corresponding principal filter.
This inclusion is order preserving, so the order relation on <code class="docutils literal notranslate"><span class="pre">Filter</span></code> can indeed be seen as the natural inclusion relation
between generalized sets. In this analogy, pushforward is analogous to the direct image.
And, indeed, <code class="docutils literal notranslate"><span class="pre">map</span> <span class="pre">f</span> <span class="pre">(&#120031;</span> <span class="pre">s)</span> <span class="pre">=</span> <span class="pre">&#120031;</span> <span class="pre">(f</span> <span class="pre">''</span> <span class="pre">s)</span></code>.</p>
<p>We can now understand intuitively why a sequence <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">:</span> <span class="pre">&#8469;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> converges to
a point <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> if and only if we have <code class="docutils literal notranslate"><span class="pre">map</span> <span class="pre">u</span> <span class="pre">atTop</span> <span class="pre">&#8804;</span> <span class="pre">&#120029;</span> <span class="pre">x&#8320;</span></code>.
The inequality means the &#8220;direct image under <code class="docutils literal notranslate"><span class="pre">u</span></code>&#8221; of
&#8220;the set of very big natural numbers&#8221; is &#8220;included&#8221; in &#8220;the set of points very close to <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code>.&#8221;</p>
<p>As promised, the definition of <code class="docutils literal notranslate"><span class="pre">Tendsto&#8322;</span></code> does not exhibit any quantifiers or sets.
It also leverages the algebraic properties of the pushforward operation.
First, each <code class="docutils literal notranslate"><span class="pre">Filter.map</span> <span class="pre">f</span></code> is monotone. And, second, <code class="docutils literal notranslate"><span class="pre">Filter.map</span></code> is compatible with
composition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="o">(</span><span class="bp">@</span><span class="n">Filter.map_mono</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">{</span><span class="n">&#945;</span> <span class="n">&#946;</span><span class="o">}</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#946;</span><span class="o">},</span> <span class="n">Monotone</span> <span class="o">(</span><span class="n">map</span> <span class="n">m</span><span class="o">))</span>

<span class="k">#check</span>
  <span class="o">(</span><span class="bp">@</span><span class="n">Filter.map_map</span> <span class="o">:</span>
    <span class="bp">&#8704;</span> <span class="o">{</span><span class="n">&#945;</span> <span class="n">&#946;</span> <span class="n">&#947;</span><span class="o">}</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">&#945;</span><span class="o">}</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#946;</span><span class="o">}</span> <span class="o">{</span><span class="n">m&#39;</span> <span class="o">:</span> <span class="n">&#946;</span> <span class="bp">&#8594;</span> <span class="n">&#947;</span><span class="o">},</span> <span class="n">map</span> <span class="n">m&#39;</span> <span class="o">(</span><span class="n">map</span> <span class="n">m</span> <span class="n">f</span><span class="o">)</span> <span class="bp">=</span> <span class="n">map</span> <span class="o">(</span><span class="n">m&#39;</span> <span class="bp">&#8728;</span> <span class="n">m</span><span class="o">)</span> <span class="n">f</span><span class="o">)</span>
</pre></div>
</div>
<p>Together these two properties allow us to prove that limits compose, yielding in one shot all 256 variants
of the composition lemma described in the introduction, and lots more.
You can practice proving the following statement using either the definition
of <code class="docutils literal notranslate"><span class="pre">Tendsto&#8321;</span></code> in terms of the
universal quantifier or the algebraic definition,
together with the two lemmas above.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="n">Z</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">{</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">G</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">Y</span><span class="o">}</span> <span class="o">{</span><span class="n">H</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">Z</span><span class="o">}</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">{</span><span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">Z</span><span class="o">}</span>
    <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Tendsto&#8321;</span> <span class="n">f</span> <span class="n">F</span> <span class="n">G</span><span class="o">)</span> <span class="o">(</span><span class="n">hg</span> <span class="o">:</span> <span class="n">Tendsto&#8321;</span> <span class="n">g</span> <span class="n">G</span> <span class="n">H</span><span class="o">)</span> <span class="o">:</span> <span class="n">Tendsto&#8321;</span> <span class="o">(</span><span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="n">F</span> <span class="n">H</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>The pushforward construction uses a map to push filters from the map source to the map target.
There also a <em>pullback</em> operation, <code class="docutils literal notranslate"><span class="pre">Filter.comap</span></code>, going in the other direction.
This generalizes the
preimage operation on sets. For any map <code class="docutils literal notranslate"><span class="pre">f</span></code>,
<code class="docutils literal notranslate"><span class="pre">Filter.map</span> <span class="pre">f</span></code> and <code class="docutils literal notranslate"><span class="pre">Filter.comap</span> <span class="pre">f</span></code> form what is known as a <em>Galois connection</em>,
which is to say, they satisfy</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">Filter.map_le_iff_le_comap</span> <span class="pre">:</span> <span class="pre">Filter.map</span> <span class="pre">f</span> <span class="pre">F</span> <span class="pre">&#8804;</span> <span class="pre">G</span> <span class="pre">&#8596;</span> <span class="pre">F</span> <span class="pre">&#8804;</span> <span class="pre">Filter.comap</span> <span class="pre">f</span> <span class="pre">G</span></code></p>
</div></blockquote>
<p>for every <code class="docutils literal notranslate"><span class="pre">F</span></code> and <code class="docutils literal notranslate"><span class="pre">G</span></code>.
This operation could be used to provided another formulation of <code class="docutils literal notranslate"><span class="pre">Tendsto</span></code> that would be provably
(but not definitionally) equivalent to the one in Mathlib.</p>
<p>The <code class="docutils literal notranslate"><span class="pre">comap</span></code> operation can be used to restrict filters to a subtype. For instance, suppose we have <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code>,
<code class="docutils literal notranslate"><span class="pre">x&#8320;</span> <span class="pre">:</span> <span class="pre">&#8477;</span></code> and <code class="docutils literal notranslate"><span class="pre">y&#8320;</span> <span class="pre">:</span> <span class="pre">&#8477;</span></code>, and suppose we want to state that <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> approaches <code class="docutils literal notranslate"><span class="pre">y&#8320;</span></code> when <code class="docutils literal notranslate"><span class="pre">x</span></code> approaches <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> within the rational numbers.
We can pull the filter <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x&#8320;</span></code> back to <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code> using the coercion map
<code class="docutils literal notranslate"><span class="pre">(&#8593;)</span> <span class="pre">:</span> <span class="pre">&#8474;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> and state <code class="docutils literal notranslate"><span class="pre">Tendsto</span> <span class="pre">(f</span> <span class="pre">&#8728;</span> <span class="pre">(&#8593;)</span> <span class="pre">:</span> <span class="pre">&#8474;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;)</span> <span class="pre">(comap</span> <span class="pre">(&#8593;)</span> <span class="pre">(&#120029;</span> <span class="pre">x&#8320;))</span> <span class="pre">(&#120029;</span> <span class="pre">y&#8320;)</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="n">y&#8320;</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span>

<span class="k">#check</span> <span class="n">comap</span> <span class="o">((</span><span class="bp">&#8593;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">)</span>

<span class="k">#check</span> <span class="n">Tendsto</span> <span class="o">(</span><span class="n">f</span> <span class="bp">&#8728;</span> <span class="o">(</span><span class="bp">&#8593;</span><span class="o">))</span> <span class="o">(</span><span class="n">comap</span> <span class="o">((</span><span class="bp">&#8593;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">))</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">y&#8320;</span><span class="o">)</span>
</pre></div>
</div>
<p>The pullback operation is also compatible with composition, but it is <em>contravariant</em>,
which is to say, it reverses the order of the arguments.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="kd">variable</span> <span class="o">{</span><span class="n">&#945;</span> <span class="n">&#946;</span> <span class="n">&#947;</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#947;</span> <span class="bp">&#8594;</span> <span class="n">&#946;</span><span class="o">}</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#946;</span> <span class="bp">&#8594;</span> <span class="n">&#945;</span><span class="o">}</span>

<span class="k">#check</span> <span class="o">(</span><span class="n">comap_comap</span> <span class="o">:</span> <span class="n">comap</span> <span class="n">m</span> <span class="o">(</span><span class="n">comap</span> <span class="n">n</span> <span class="n">F</span><span class="o">)</span> <span class="bp">=</span> <span class="n">comap</span> <span class="o">(</span><span class="n">n</span> <span class="bp">&#8728;</span> <span class="n">m</span><span class="o">)</span> <span class="n">F</span><span class="o">)</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>Let&#8217;s now shift attention to the plane <code class="docutils literal notranslate"><span class="pre">&#8477;</span> <span class="pre">&#215;</span> <span class="pre">&#8477;</span></code> and try to understand how the neighborhoods of a point
<code class="docutils literal notranslate"><span class="pre">(x&#8320;,</span> <span class="pre">y&#8320;)</span></code> are related to <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x&#8320;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">y&#8320;</span></code>. There is a product operation
<code class="docutils literal notranslate"><span class="pre">Filter.prod</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">Y</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">(X</span> <span class="pre">&#215;</span> <span class="pre">Y)</span></code>, denoted by <code class="docutils literal notranslate"><span class="pre">&#215;&#738;</span></code>, which answers this question:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#120029;</span> <span class="o">(</span><span class="n">x&#8320;</span><span class="o">,</span> <span class="n">y&#8320;</span><span class="o">)</span> <span class="bp">=</span> <span class="bp">&#120029;</span> <span class="n">x&#8320;</span> <span class="bp">&#215;&#738;</span> <span class="bp">&#120029;</span> <span class="n">y&#8320;</span> <span class="o">:=</span>
  <span class="n">nhds_prod_eq</span>
</pre></div>
</div>
<p>The product operation is defined in terms of the pullback operation and the <code class="docutils literal notranslate"><span class="pre">inf</span></code> operation:</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">&#215;&#738;</span> <span class="pre">G</span> <span class="pre">=</span> <span class="pre">(comap</span> <span class="pre">Prod.fst</span> <span class="pre">F)</span> <span class="pre">&#8851;</span> <span class="pre">(comap</span> <span class="pre">Prod.snd</span> <span class="pre">G)</span></code>.</p>
</div></blockquote>
<p>Here the <code class="docutils literal notranslate"><span class="pre">inf</span></code> operation refers to the lattice structure on <code class="docutils literal notranslate"><span class="pre">Filter</span> <span class="pre">X</span></code> for any type <code class="docutils literal notranslate"><span class="pre">X</span></code>, whereby
<code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">&#8851;</span> <span class="pre">G</span></code> is the greatest filter that is smaller than both <code class="docutils literal notranslate"><span class="pre">F</span></code> and <code class="docutils literal notranslate"><span class="pre">G</span></code>.
Thus the <code class="docutils literal notranslate"><span class="pre">inf</span></code> operation generalizes the notion of the intersection of sets.</p>
<p>A lot of proofs in Mathlib use all of the aforementioned structure (<code class="docutils literal notranslate"><span class="pre">map</span></code>, <code class="docutils literal notranslate"><span class="pre">comap</span></code>, <code class="docutils literal notranslate"><span class="pre">inf</span></code>, <code class="docutils literal notranslate"><span class="pre">sup</span></code>, and <code class="docutils literal notranslate"><span class="pre">prod</span></code>)
to give algebraic proofs about convergence without ever referring to members of filters.
You can practice doing this in a proof of the following lemma, unfolding the definition of <code class="docutils literal notranslate"><span class="pre">Tendsto</span></code>
and <code class="docutils literal notranslate"><span class="pre">Filter.prod</span></code> if needed.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="n">le_inf_iff</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="n">y&#8320;</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Tendsto</span> <span class="n">f</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="o">(</span><span class="n">x&#8320;</span><span class="o">,</span> <span class="n">y&#8320;</span><span class="o">))</span> <span class="bp">&#8596;</span>
      <span class="n">Tendsto</span> <span class="o">(</span><span class="n">Prod.fst</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">)</span> <span class="bp">&#8743;</span> <span class="n">Tendsto</span> <span class="o">(</span><span class="n">Prod.snd</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">y&#8320;</span><span class="o">)</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>The ordered type <code class="docutils literal notranslate"><span class="pre">Filter</span> <span class="pre">X</span></code> is actually a <em>complete</em> lattice,
which is to say, there is a bottom element, there is a top element, and
every set of filters on <code class="docutils literal notranslate"><span class="pre">X</span></code> has an <code class="docutils literal notranslate"><span class="pre">Inf</span></code> and a <code class="docutils literal notranslate"><span class="pre">Sup</span></code>.</p>
<p>Note that given the second property in the definition of a filter
(if <code class="docutils literal notranslate"><span class="pre">U</span></code> belongs to <code class="docutils literal notranslate"><span class="pre">F</span></code> then anything larger than <code class="docutils literal notranslate"><span class="pre">U</span></code> also belongs to <code class="docutils literal notranslate"><span class="pre">F</span></code>),
the first property
(the set of all inhabitants of <code class="docutils literal notranslate"><span class="pre">X</span></code> belongs to <code class="docutils literal notranslate"><span class="pre">F</span></code>) is
equivalent to the property that <code class="docutils literal notranslate"><span class="pre">F</span></code> is not the empty collection of sets.
This shouldn&#8217;t be confused with the more subtle question as to whether
the empty set is an <em>element</em> of <code class="docutils literal notranslate"><span class="pre">F</span></code>. The
definition of a filter does not prohibit <code class="docutils literal notranslate"><span class="pre">&#8709;</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code>,
but if the empty set is in <code class="docutils literal notranslate"><span class="pre">F</span></code> then
every set is in <code class="docutils literal notranslate"><span class="pre">F</span></code>, which is to say, <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">U</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">X,</span> <span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code>.
In this case, <code class="docutils literal notranslate"><span class="pre">F</span></code> is a rather trivial filter, which is precisely the
bottom element of the complete lattice <code class="docutils literal notranslate"><span class="pre">Filter</span> <span class="pre">X</span></code>.
This contrasts with the definition of filters in
Bourbaki, which doesn&#8217;t allow filters containing the empty set.</p>
<p>Because we include the trivial filter in our definition, we sometimes need to explicitly assume
nontriviality in some lemmas.
In return, however, the theory has nicer global properties.
We have already seen that including the trivial filter gives us a
bottom element. It also allows us to define <code class="docutils literal notranslate"><span class="pre">principal</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">X</span></code>,
which maps  <code class="docutils literal notranslate"><span class="pre">&#8709;</span></code> to <code class="docutils literal notranslate"><span class="pre">&#8869;</span></code>, without adding a precondition to rule out the empty set.
And it allows us to define the pullback operation without a precondition as well.
Indeed, it can happen that <code class="docutils literal notranslate"><span class="pre">comap</span> <span class="pre">f</span> <span class="pre">F</span> <span class="pre">=</span> <span class="pre">&#8869;</span></code> although <code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">&#8800;</span> <span class="pre">&#8869;</span></code>. For instance,
given <code class="docutils literal notranslate"><span class="pre">x&#8320;</span> <span class="pre">:</span> <span class="pre">&#8477;</span></code> and <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">&#8477;</span></code>, the pullback of <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x&#8320;</span></code> under the coercion
from the subtype corresponding to <code class="docutils literal notranslate"><span class="pre">s</span></code> is nontrivial if and only if <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> belongs to the
closure of <code class="docutils literal notranslate"><span class="pre">s</span></code>.</p>
<p>In order to manage lemmas that do need to assume some filter is nontrivial, Mathlib has
a type class <code class="docutils literal notranslate"><span class="pre">Filter.NeBot</span></code>, and the library has lemmas that assume
<code class="docutils literal notranslate"><span class="pre">(F</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">X)</span> <span class="pre">[F.NeBot]</span></code>. The instance database knows, for example, that <code class="docutils literal notranslate"><span class="pre">(atTop</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">&#8469;).NeBot</span></code>,
and it knows that pushing forward a nontrivial filter gives a nontrivial filter.
As a result, a lemma assuming <code class="docutils literal notranslate"><span class="pre">[F.NeBot]</span></code> will automatically apply to <code class="docutils literal notranslate"><span class="pre">map</span> <span class="pre">u</span> <span class="pre">atTop</span></code> for any sequence <code class="docutils literal notranslate"><span class="pre">u</span></code>.</p>
<p>Our tour of the algebraic properties of filters and their relation to limits is essentially done,
but we have not yet justified our claim to have recaptured the usual limit notions.
Superficially, it may seem that <code class="docutils literal notranslate"><span class="pre">Tendsto</span> <span class="pre">u</span> <span class="pre">atTop</span> <span class="pre">(&#120029;</span> <span class="pre">x&#8320;)</span></code>
is stronger than the notion of convergence defined in <a class="reference internal" href="C03_Logic.html#sequences-and-convergence"><span class="std std-numref">Section 3.6</span></a> because we ask that <em>every</em> neighborhood of <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code>
has a preimage belonging to <code class="docutils literal notranslate"><span class="pre">atTop</span></code>, whereas the usual definition only requires
this for the standard neighborhoods <code class="docutils literal notranslate"><span class="pre">Ioo</span> <span class="pre">(x&#8320;</span> <span class="pre">-</span> <span class="pre">&#949;)</span> <span class="pre">(x&#8320;</span> <span class="pre">+</span> <span class="pre">&#949;)</span></code>.
The key is that, by definition, every neighborhood contains such a standard one.
This observation leads to the notion of a <em>filter basis</em>.</p>
<p>Given <code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">X</span></code>,
a family of sets <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">&#953;</span> <span class="pre">&#8594;</span> <span class="pre">Set</span> <span class="pre">X</span></code> is a basis for <code class="docutils literal notranslate"><span class="pre">F</span></code> if for every set <code class="docutils literal notranslate"><span class="pre">U</span></code>,
we have <code class="docutils literal notranslate"><span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code> if and only if it contains some <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">i</span></code>. In other words, formally speaking,
<code class="docutils literal notranslate"><span class="pre">s</span></code> is a basis if it satisfies
<code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">U</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">X,</span> <span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F</span> <span class="pre">&#8596;</span> <span class="pre">&#8707;</span> <span class="pre">i,</span> <span class="pre">s</span> <span class="pre">i</span> <span class="pre">&#8838;</span> <span class="pre">U</span></code>. It is even more flexible to consider
a predicate on <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> that selects only some of the values <code class="docutils literal notranslate"><span class="pre">i</span></code> in the indexing type.
In the case of <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x&#8320;</span></code>, we want <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> to be <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>, we write <code class="docutils literal notranslate"><span class="pre">&#949;</span></code> for <code class="docutils literal notranslate"><span class="pre">i</span></code>, and the predicate should select the positive values of <code class="docutils literal notranslate"><span class="pre">&#949;</span></code>.
So the fact that the sets <code class="docutils literal notranslate"><span class="pre">Ioo</span>&#160; <span class="pre">(x&#8320;</span> <span class="pre">-</span> <span class="pre">&#949;)</span> <span class="pre">(x&#8320;</span> <span class="pre">+</span> <span class="pre">&#949;)</span></code> form a basis for the
neighborhood topology on <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> is stated as follows:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">HasBasis</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">)</span> <span class="o">(</span><span class="k">fun</span> <span class="n">&#949;</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#8614;</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">&#949;</span><span class="o">)</span> <span class="k">fun</span> <span class="n">&#949;</span> <span class="bp">&#8614;</span> <span class="n">Ioo</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="bp">-</span> <span class="n">&#949;</span><span class="o">)</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="bp">+</span> <span class="n">&#949;</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">nhds_basis_Ioo_pos</span> <span class="n">x&#8320;</span>
</pre></div>
</div>
<p>There is also a nice basis for the filter <code class="docutils literal notranslate"><span class="pre">atTop</span></code>. The lemma
<code class="docutils literal notranslate"><span class="pre">Filter.has_basis.tendsto_iff</span></code> allows
us to reformulate a statement of the form <code class="docutils literal notranslate"><span class="pre">Tendsto</span> <span class="pre">f</span> <span class="pre">F</span> <span class="pre">G</span></code>
given bases for <code class="docutils literal notranslate"><span class="pre">F</span></code> and <code class="docutils literal notranslate"><span class="pre">G</span></code>.
Putting these pieces together gives us essentially the notion of convergence
that we used in <a class="reference internal" href="C03_Logic.html#sequences-and-convergence"><span class="std std-numref">Section 3.6</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">)</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">N</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">n</span> <span class="bp">&#8805;</span> <span class="n">N</span><span class="o">,</span> <span class="n">u</span> <span class="n">n</span> <span class="bp">&#8712;</span> <span class="n">Ioo</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="bp">-</span> <span class="n">&#949;</span><span class="o">)</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="bp">+</span> <span class="n">&#949;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="o">:</span> <span class="n">atTop.HasBasis</span> <span class="o">(</span><span class="k">fun</span> <span class="n">_</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8614;</span> <span class="n">True</span><span class="o">)</span> <span class="n">Ici</span> <span class="o">:=</span> <span class="n">atTop_basis</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">this.tendsto_iff</span> <span class="o">(</span><span class="n">nhds_basis_Ioo_pos</span> <span class="n">x&#8320;</span><span class="o">)]</span>
  <span class="n">simp</span>
</pre></div>
</div>
<p>We now show how filters facilitate working with properties that hold for sufficiently large numbers
or for points that are sufficiently close to a given point. In <a class="reference internal" href="C03_Logic.html#sequences-and-convergence"><span class="std std-numref">Section 3.6</span></a>, we were often faced with the situation where
we knew that some property <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">n</span></code> holds for sufficiently large <code class="docutils literal notranslate"><span class="pre">n</span></code> and that some
other property <code class="docutils literal notranslate"><span class="pre">Q</span> <span class="pre">n</span></code> holds for sufficiently large <code class="docutils literal notranslate"><span class="pre">n</span></code>.
Using <code class="docutils literal notranslate"><span class="pre">cases</span></code> twice gave us <code class="docutils literal notranslate"><span class="pre">N_P</span></code> and <code class="docutils literal notranslate"><span class="pre">N_Q</span></code> satisfying
<code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">n</span> <span class="pre">&#8805;</span> <span class="pre">N_P,</span> <span class="pre">P</span> <span class="pre">n</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">n</span> <span class="pre">&#8805;</span> <span class="pre">N_Q,</span> <span class="pre">Q</span> <span class="pre">n</span></code>. Using <code class="docutils literal notranslate"><span class="pre">set</span> <span class="pre">N</span> <span class="pre">:=</span> <span class="pre">max</span> <span class="pre">N_P</span> <span class="pre">N_Q</span></code>, we could
eventually prove <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">n</span> <span class="pre">&#8805;</span> <span class="pre">N,</span> <span class="pre">P</span> <span class="pre">n</span> <span class="pre">&#8743;</span> <span class="pre">Q</span> <span class="pre">n</span></code>.
Doing this repeatedly becomes tiresome.</p>
<p>We can do better by noting that the statement &#8220;<code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">n</span></code> and <code class="docutils literal notranslate"><span class="pre">Q</span> <span class="pre">n</span></code> hold for large enough <code class="docutils literal notranslate"><span class="pre">n</span></code>&#8221; means
that we have <code class="docutils literal notranslate"><span class="pre">{n</span> <span class="pre">|</span> <span class="pre">P</span> <span class="pre">n}</span> <span class="pre">&#8712;</span> <span class="pre">atTop</span></code> and <code class="docutils literal notranslate"><span class="pre">{n</span> <span class="pre">|</span> <span class="pre">Q</span> <span class="pre">n}</span> <span class="pre">&#8712;</span> <span class="pre">atTop</span></code>.
The fact that <code class="docutils literal notranslate"><span class="pre">atTop</span></code> is a filter implies that the intersection of two elements of <code class="docutils literal notranslate"><span class="pre">atTop</span></code>
is again in <code class="docutils literal notranslate"><span class="pre">atTop</span></code>, so we have <code class="docutils literal notranslate"><span class="pre">{n</span> <span class="pre">|</span> <span class="pre">P</span> <span class="pre">n</span> <span class="pre">&#8743;</span> <span class="pre">Q</span> <span class="pre">n}</span> <span class="pre">&#8712;</span> <span class="pre">atTop</span></code>.
Writing <code class="docutils literal notranslate"><span class="pre">{n</span> <span class="pre">|</span> <span class="pre">P</span> <span class="pre">n}</span> <span class="pre">&#8712;</span> <span class="pre">atTop</span></code> is unpleasant,
but we can use the more suggestive notation <code class="docutils literal notranslate"><span class="pre">&#8704;&#7584;</span> <span class="pre">n</span> <span class="pre">in</span> <span class="pre">atTop,</span> <span class="pre">P</span> <span class="pre">n</span></code>.
Here the superscripted <code class="docutils literal notranslate"><span class="pre">f</span></code> stands for &#8220;Filter.&#8221;
You can think of the notation as saying that for all <code class="docutils literal notranslate"><span class="pre">n</span></code> in the &#8220;set of very large numbers,&#8221; <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">n</span></code> holds. The <code class="docutils literal notranslate"><span class="pre">&#8704;&#7584;</span></code>
notation stands for <code class="docutils literal notranslate"><span class="pre">Filter.Eventually</span></code>, and the lemma <code class="docutils literal notranslate"><span class="pre">Filter.Eventually.and</span></code> uses the intersection property of filters to do what we just described:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">P</span> <span class="n">Q</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span><span class="o">)</span> <span class="o">(</span><span class="n">hP</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">P</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">hQ</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">Q</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">P</span> <span class="n">n</span> <span class="bp">&#8743;</span> <span class="n">Q</span> <span class="n">n</span> <span class="o">:=</span>
  <span class="n">hP.and</span> <span class="n">hQ</span>
</pre></div>
</div>
<p>This notation is so convenient and intuitive that we also have specializations
when <code class="docutils literal notranslate"><span class="pre">P</span></code> is an equality or inequality statement. For example, let <code class="docutils literal notranslate"><span class="pre">u</span></code> and <code class="docutils literal notranslate"><span class="pre">v</span></code> be
two sequences of real numbers, and let us show that if
<code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">n</span></code> and <code class="docutils literal notranslate"><span class="pre">v</span> <span class="pre">n</span></code> coincide for sufficiently large <code class="docutils literal notranslate"><span class="pre">n</span></code> then
<code class="docutils literal notranslate"><span class="pre">u</span></code> tends to <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code> if and only if <code class="docutils literal notranslate"><span class="pre">v</span></code> tends to <code class="docutils literal notranslate"><span class="pre">x&#8320;</span></code>.
First we&#8217;ll use the generic <code class="docutils literal notranslate"><span class="pre">Eventually</span></code> and then the one
specialized for the equality predicate, <code class="docutils literal notranslate"><span class="pre">EventuallyEq</span></code>. The two statements are
definitionally equivalent so the same proof work in both cases.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">u</span> <span class="n">v</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">u</span> <span class="n">n</span> <span class="bp">=</span> <span class="n">v</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">)</span> <span class="bp">&#8596;</span> <span class="n">Tendsto</span> <span class="n">v</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">tendsto_congr&#39;</span> <span class="n">h</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">u</span> <span class="n">v</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">u</span> <span class="bp">=&#7584;</span><span class="o">[</span><span class="n">atTop</span><span class="o">]</span> <span class="n">v</span><span class="o">)</span> <span class="o">(</span><span class="n">x&#8320;</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">)</span> <span class="bp">&#8596;</span> <span class="n">Tendsto</span> <span class="n">v</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x&#8320;</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">tendsto_congr&#39;</span> <span class="n">h</span>
</pre></div>
</div>
<p>It is instructive to review the definition of filters in terms of <code class="docutils literal notranslate"><span class="pre">Eventually</span></code>.
Given <code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">:</span> <span class="pre">Filter</span> <span class="pre">X</span></code>, for any predicates <code class="docutils literal notranslate"><span class="pre">P</span></code> and <code class="docutils literal notranslate"><span class="pre">Q</span></code> on <code class="docutils literal notranslate"><span class="pre">X</span></code>,</p>
<ul class="simple">
<li><p>the condition <code class="docutils literal notranslate"><span class="pre">univ</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code> ensures <code class="docutils literal notranslate"><span class="pre">(&#8704;</span> <span class="pre">x,</span> <span class="pre">P</span> <span class="pre">x)</span> <span class="pre">&#8594;</span> <span class="pre">&#8704;&#7584;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">F,</span> <span class="pre">P</span> <span class="pre">x</span></code>,</p></li>
<li><p>the condition <code class="docutils literal notranslate"><span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F</span> <span class="pre">&#8594;</span> <span class="pre">U</span> <span class="pre">&#8838;</span> <span class="pre">V</span> <span class="pre">&#8594;</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code> ensures <code class="docutils literal notranslate"><span class="pre">(&#8704;&#7584;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">F,</span> <span class="pre">P</span> <span class="pre">x)</span> <span class="pre">&#8594;</span> <span class="pre">(&#8704;</span> <span class="pre">x,</span> <span class="pre">P</span> <span class="pre">x</span> <span class="pre">&#8594;</span> <span class="pre">Q</span> <span class="pre">x)</span> <span class="pre">&#8594;</span> <span class="pre">&#8704;&#7584;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">F,</span> <span class="pre">Q</span> <span class="pre">x</span></code>, and</p></li>
<li><p>the condition <code class="docutils literal notranslate"><span class="pre">U</span> <span class="pre">&#8712;</span> <span class="pre">F</span> <span class="pre">&#8594;</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">F</span> <span class="pre">&#8594;</span> <span class="pre">U</span> <span class="pre">&#8745;</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">F</span></code> ensures <code class="docutils literal notranslate"><span class="pre">(&#8704;&#7584;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">F,</span> <span class="pre">P</span> <span class="pre">x)</span> <span class="pre">&#8594;</span> <span class="pre">(&#8704;&#7584;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">F,</span> <span class="pre">Q</span> <span class="pre">x)</span> <span class="pre">&#8594;</span> <span class="pre">&#8704;&#7584;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">F,</span> <span class="pre">P</span> <span class="pre">x</span> <span class="pre">&#8743;</span> <span class="pre">Q</span> <span class="pre">x</span></code>.</p></li>
</ul>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="n">eventually_of_forall</span>
<span class="k">#check</span> <span class="n">Eventually.mono</span>
<span class="k">#check</span> <span class="n">Eventually.and</span>
</pre></div>
</div>
<p>The second item, corresponding to <code class="docutils literal notranslate"><span class="pre">Eventually.mono</span></code>, supports nice ways
of using filters, especially when combined
with <code class="docutils literal notranslate"><span class="pre">Eventually.and</span></code>. The <code class="docutils literal notranslate"><span class="pre">filter_upwards</span></code> tactic allows us to combine them.
Compare:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">P</span> <span class="n">Q</span> <span class="n">R</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span><span class="o">)</span> <span class="o">(</span><span class="n">hP</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">P</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">hQ</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">Q</span> <span class="n">n</span><span class="o">)</span>
    <span class="o">(</span><span class="n">hR</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">P</span> <span class="n">n</span> <span class="bp">&#8743;</span> <span class="n">Q</span> <span class="n">n</span> <span class="bp">&#8594;</span> <span class="n">R</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">R</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="o">(</span><span class="n">hP.and</span> <span class="o">(</span><span class="n">hQ.and</span> <span class="n">hR</span><span class="o">))</span><span class="bp">.</span><span class="n">mono</span>
  <span class="n">rintro</span> <span class="n">n</span> <span class="o">&#10216;</span><span class="n">h</span><span class="o">,</span> <span class="n">h&#39;</span><span class="o">,</span> <span class="n">h&#39;&#39;</span><span class="o">&#10217;</span>
  <span class="n">exact</span> <span class="n">h&#39;&#39;</span> <span class="o">&#10216;</span><span class="n">h</span><span class="o">,</span> <span class="n">h&#39;</span><span class="o">&#10217;</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">P</span> <span class="n">Q</span> <span class="n">R</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span><span class="o">)</span> <span class="o">(</span><span class="n">hP</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">P</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">hQ</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">Q</span> <span class="n">n</span><span class="o">)</span>
    <span class="o">(</span><span class="n">hR</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">P</span> <span class="n">n</span> <span class="bp">&#8743;</span> <span class="n">Q</span> <span class="n">n</span> <span class="bp">&#8594;</span> <span class="n">R</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">R</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">filter_upwards</span> <span class="o">[</span><span class="n">hP</span><span class="o">,</span> <span class="n">hQ</span><span class="o">,</span> <span class="n">hR</span><span class="o">]</span> <span class="k">with</span> <span class="n">n</span> <span class="n">h</span> <span class="n">h&#39;</span> <span class="n">h&#39;&#39;</span>
  <span class="n">exact</span> <span class="n">h&#39;&#39;</span> <span class="o">&#10216;</span><span class="n">h</span><span class="o">,</span> <span class="n">h&#39;</span><span class="o">&#10217;</span>
</pre></div>
</div>
<p>Readers who know about measure theory will note that the filter <code class="docutils literal notranslate"><span class="pre">&#956;.ae</span></code> of sets whose complement has measure zero
(aka &#8220;the set consisting of almost every point&#8221;) is not very useful as the source or target of <code class="docutils literal notranslate"><span class="pre">Tendsto</span></code>, but it can be conveniently
used with <code class="docutils literal notranslate"><span class="pre">Eventually</span></code> to say that a property holds for almost every point.</p>
<p>There is a dual version of <code class="docutils literal notranslate"><span class="pre">&#8704;&#7584;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">F,</span> <span class="pre">P</span> <span class="pre">x</span></code>, which is occasionally useful:
<code class="docutils literal notranslate"><span class="pre">&#8707;&#7584;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">F,</span> <span class="pre">P</span> <span class="pre">x</span></code> means
<code class="docutils literal notranslate"><span class="pre">{x</span> <span class="pre">|</span> <span class="pre">&#172;P</span> <span class="pre">x}</span> <span class="pre">&#8713;</span> <span class="pre">F</span></code>. For example, <code class="docutils literal notranslate"><span class="pre">&#8707;&#7584;</span> <span class="pre">n</span> <span class="pre">in</span> <span class="pre">atTop,</span> <span class="pre">P</span> <span class="pre">n</span></code> means there are arbitrarily large <code class="docutils literal notranslate"><span class="pre">n</span></code> such that <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">n</span></code> holds.
The <code class="docutils literal notranslate"><span class="pre">&#8707;&#7584;</span></code> notation stands for <code class="docutils literal notranslate"><span class="pre">Filter.Frequently</span></code>.</p>
<p>For a more sophisticated example, consider the following statement about a sequence
<code class="docutils literal notranslate"><span class="pre">u</span></code>, a set <code class="docutils literal notranslate"><span class="pre">M</span></code>, and a value <code class="docutils literal notranslate"><span class="pre">x</span></code>:</p>
<blockquote>
<div><p>If <code class="docutils literal notranslate"><span class="pre">u</span></code> converges to <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">n</span></code> belongs to <code class="docutils literal notranslate"><span class="pre">M</span></code> for
sufficiently large <code class="docutils literal notranslate"><span class="pre">n</span></code> then <code class="docutils literal notranslate"><span class="pre">x</span></code> is in the closure of <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
</div></blockquote>
<p>This can be formalized as follows:</p>
<blockquote>
<div><p><code class="docutils literal notranslate"><span class="pre">Tendsto</span> <span class="pre">u</span> <span class="pre">atTop</span> <span class="pre">(&#120029;</span> <span class="pre">x)</span> <span class="pre">&#8594;</span> <span class="pre">(&#8704;&#7584;</span> <span class="pre">n</span> <span class="pre">in</span> <span class="pre">atTop,</span> <span class="pre">u</span> <span class="pre">n</span> <span class="pre">&#8712;</span> <span class="pre">M)</span> <span class="pre">&#8594;</span> <span class="pre">x</span> <span class="pre">&#8712;</span> <span class="pre">closure</span> <span class="pre">M</span></code>.</p>
</div></blockquote>
<p>This is a special case of the theorem <code class="docutils literal notranslate"><span class="pre">mem_closure_of_tendsto</span></code> from the
topology library.
See if you can prove it using the quoted lemmas,
using the fact that <code class="docutils literal notranslate"><span class="pre">ClusterPt</span> <span class="pre">x</span> <span class="pre">F</span></code> means <code class="docutils literal notranslate"><span class="pre">(&#120029;</span> <span class="pre">x</span> <span class="pre">&#8851;</span> <span class="pre">F).NeBot</span></code> and that,
by definition, the assumption <code class="docutils literal notranslate"><span class="pre">&#8704;&#7584;</span> <span class="pre">n</span> <span class="pre">in</span> <span class="pre">atTop,</span> <span class="pre">u</span> <span class="pre">n</span> <span class="pre">&#8712;</span> <span class="pre">M</span></code> means  <code class="docutils literal notranslate"><span class="pre">M</span> <span class="pre">&#8712;</span> <span class="pre">map</span> <span class="pre">u</span> <span class="pre">atTop</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="n">mem_closure_iff_clusterPt</span>
<span class="k">#check</span> <span class="n">le_principal_iff</span>
<span class="k">#check</span> <span class="n">neBot_of_le</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">M</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">hux</span> <span class="o">:</span> <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x</span><span class="o">))</span>
    <span class="o">(</span><span class="n">huM</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">n</span> <span class="k">in</span> <span class="n">atTop</span><span class="o">,</span> <span class="n">u</span> <span class="n">n</span> <span class="bp">&#8712;</span> <span class="n">M</span><span class="o">)</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">closure</span> <span class="n">M</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="metric-spaces">
<span id="index-2"></span><span id="id3"></span><h2><span class="section-number">9.2. </span>Metric spaces<a class="headerlink" href="#metric-spaces" title="Permalink to this heading">&#61633;</a></h2>
<p>Examples in the previous section focus on sequences of real numbers. In this section we will go up a bit in generality and focus on
metric spaces. A metric space is a type <code class="docutils literal notranslate"><span class="pre">X</span></code> equipped with a distance function <code class="docutils literal notranslate"><span class="pre">dist</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> which is a generalization of
the function <code class="docutils literal notranslate"><span class="pre">fun</span> <span class="pre">x</span> <span class="pre">y</span> <span class="pre">&#8614;</span> <span class="pre">|x</span> <span class="pre">-</span> <span class="pre">y|</span></code> from the case where <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">=</span> <span class="pre">&#8477;</span></code>.</p>
<p>Introducing such a space is easy and we will check all properties required from the distance function.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span> <span class="o">{</span><span class="n">X</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">X</span><span class="o">)</span>

<span class="k">#check</span> <span class="o">(</span><span class="n">dist</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span>
<span class="k">#check</span> <span class="o">(</span><span class="n">dist_nonneg</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">dist</span> <span class="n">a</span> <span class="n">b</span><span class="o">)</span>
<span class="k">#check</span> <span class="o">(</span><span class="n">dist_eq_zero</span> <span class="o">:</span> <span class="n">dist</span> <span class="n">a</span> <span class="n">b</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">&#8596;</span> <span class="n">a</span> <span class="bp">=</span> <span class="n">b</span><span class="o">)</span>
<span class="k">#check</span> <span class="o">(</span><span class="n">dist_comm</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">dist</span> <span class="n">a</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">dist</span> <span class="n">b</span> <span class="n">a</span><span class="o">)</span>
<span class="k">#check</span> <span class="o">(</span><span class="n">dist_triangle</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">dist</span> <span class="n">a</span> <span class="n">c</span> <span class="bp">&#8804;</span> <span class="n">dist</span> <span class="n">a</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">dist</span> <span class="n">b</span> <span class="n">c</span><span class="o">)</span>
</pre></div>
</div>
<p>Note we also have variants where the distance can be infinite or where <code class="docutils literal notranslate"><span class="pre">dist</span> <span class="pre">a</span> <span class="pre">b</span></code> can be zero without having <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">=</span> <span class="pre">b</span></code> or both.
They are called <code class="docutils literal notranslate"><span class="pre">EMetricSpace</span></code>, <code class="docutils literal notranslate"><span class="pre">PseudoMetricSpace</span></code> and <code class="docutils literal notranslate"><span class="pre">PseudoEMetricSpace</span></code> respectively (here &#8220;e&#8221; stands for &#8220;extended&#8221;).</p>
<p>Note that our journey from <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> to metric spaces jumped over the special case of normed spaces that also require linear algebra and
will be explained as part of the calculus chapter.</p>
<section id="convergence-and-continuity">
<h3><span class="section-number">9.2.1. </span>Convergence and continuity<a class="headerlink" href="#convergence-and-continuity" title="Permalink to this heading">&#61633;</a></h3>
<p>Using distance functions, we can already define convergent sequences and continuous functions between metric spaces.
They are actually defined in a more general setting covered in the next section,
but we have lemmas recasting the definition is terms of distances.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span>
    <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">a</span><span class="o">)</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">N</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">n</span> <span class="bp">&#8805;</span> <span class="n">N</span><span class="o">,</span> <span class="n">dist</span> <span class="o">(</span><span class="n">u</span> <span class="n">n</span><span class="o">)</span> <span class="n">a</span> <span class="bp">&lt;</span> <span class="n">&#949;</span> <span class="o">:=</span>
  <span class="n">Metric.tendsto_atTop</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">:</span>
    <span class="n">Continuous</span> <span class="n">f</span> <span class="bp">&#8596;</span>
      <span class="bp">&#8704;</span> <span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">&#948;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">x&#39;</span><span class="o">,</span> <span class="n">dist</span> <span class="n">x&#39;</span> <span class="n">x</span> <span class="bp">&lt;</span> <span class="n">&#948;</span> <span class="bp">&#8594;</span> <span class="n">dist</span> <span class="o">(</span><span class="n">f</span> <span class="n">x&#39;</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="n">x</span><span class="o">)</span> <span class="bp">&lt;</span> <span class="n">&#949;</span> <span class="o">:=</span>
  <span class="n">Metric.continuous_iff</span>
</pre></div>
</div>
<p id="index-3">A <em>lot</em> of lemmas have some continuity assumptions, so we end up proving a lot of continuity results and there
is a <code class="docutils literal notranslate"><span class="pre">continuity</span></code> tactic devoted to this task. Let&#8217;s prove a continuity statement that will be needed
in an exercise below. Notice that Lean knows how to treat a product of two metric spaces as a metric space, so
it makes sense to consider continuous functions from <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">&#215;</span> <span class="pre">X</span></code> to <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>.
In particular the (uncurried version of the) distance function is such a function.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Continuous</span> <span class="k">fun</span> <span class="n">p</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#215;</span> <span class="n">X</span> <span class="bp">&#8614;</span> <span class="n">dist</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.1</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">continuity</span>
</pre></div>
</div>
<p>This tactic is a bit slow, so it is also useful to know
how to do it by hand. We first need to use that <code class="docutils literal notranslate"><span class="pre">fun</span> <span class="pre">p</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#215;</span> <span class="pre">X</span> <span class="pre">&#8614;</span> <span class="pre">f</span> <span class="pre">p.1</span></code> is continuous because it
is the composition of <code class="docutils literal notranslate"><span class="pre">f</span></code>, which is continuous by assumption <code class="docutils literal notranslate"><span class="pre">hf</span></code>, and the projection <code class="docutils literal notranslate"><span class="pre">prod.fst</span></code> whose continuity
is the content of the lemma <code class="docutils literal notranslate"><span class="pre">continuous_fst</span></code>. The composition property is <code class="docutils literal notranslate"><span class="pre">Continuous.comp</span></code> which is
in the <code class="docutils literal notranslate"><span class="pre">Continuous</span></code> namespace so we can use dot notation to compress
<code class="docutils literal notranslate"><span class="pre">Continuous.comp</span> <span class="pre">hf</span> <span class="pre">continuous_fst</span></code> into <code class="docutils literal notranslate"><span class="pre">hf.comp</span> <span class="pre">continuous_fst</span></code> which is actually more readable
since it really reads as composing our assumption and our lemma.
We can do the same for the second component to get continuity of <code class="docutils literal notranslate"><span class="pre">fun</span> <span class="pre">p</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#215;</span> <span class="pre">X</span> <span class="pre">&#8614;</span> <span class="pre">f</span> <span class="pre">p.2</span></code>. We then assemble
those two continuities using <code class="docutils literal notranslate"><span class="pre">Continuous.prod_mk</span></code> to get
<code class="docutils literal notranslate"><span class="pre">(hf.comp</span> <span class="pre">continuous_fst).prod_mk</span> <span class="pre">(hf.comp</span> <span class="pre">continuous_snd)</span> <span class="pre">:</span> <span class="pre">Continuous</span> <span class="pre">(fun</span> <span class="pre">p</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#215;</span> <span class="pre">X</span> <span class="pre">&#8614;</span> <span class="pre">(f</span> <span class="pre">p.1,</span> <span class="pre">f</span> <span class="pre">p.2))</span></code>
and compose once more to get our full proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Continuous</span> <span class="k">fun</span> <span class="n">p</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#215;</span> <span class="n">X</span> <span class="bp">&#8614;</span> <span class="n">dist</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.1</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.2</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">continuous_dist.comp</span> <span class="o">((</span><span class="n">hf.comp</span> <span class="n">continuous_fst</span><span class="o">)</span><span class="bp">.</span><span class="n">prod_mk</span> <span class="o">(</span><span class="n">hf.comp</span> <span class="n">continuous_snd</span><span class="o">))</span>
</pre></div>
</div>
<p>The combination of <code class="docutils literal notranslate"><span class="pre">Continuous.prod_mk</span></code> and <code class="docutils literal notranslate"><span class="pre">continuous_dist</span></code> via <code class="docutils literal notranslate"><span class="pre">Continuous.comp</span></code> feels clunky,
even when heavily using dot notation as above. A more serious issue is that this nice proof requires a lot of
planning. Lean accepts the above proof term because it is a full term proving a statement which is
definitionally equivalent to our goal, the crucial definition to unfold being that of a composition of functions.
Indeed our target function <code class="docutils literal notranslate"><span class="pre">fun</span> <span class="pre">p</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#215;</span> <span class="pre">X</span> <span class="pre">&#8614;</span> <span class="pre">dist</span> <span class="pre">(f</span> <span class="pre">p.1)</span> <span class="pre">(f</span> <span class="pre">p.2)</span></code> is not presented as a composition.
The proof term we provided proves continuity of <code class="docutils literal notranslate"><span class="pre">dist</span> <span class="pre">&#8728;</span> <span class="pre">(fun</span> <span class="pre">p</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#215;</span> <span class="pre">X</span> <span class="pre">&#8614;</span> <span class="pre">(f</span> <span class="pre">p.1,</span> <span class="pre">f</span> <span class="pre">p.2))</span></code> which happens
to be definitionally equal to our target function. But if we try to build this proof gradually using
tactics starting with <code class="docutils literal notranslate"><span class="pre">apply</span> <span class="pre">continuous_dist.comp</span></code> then Lean&#8217;s elaborator will fail to recognize a
composition and refuse to apply this lemma. It is especially bad at this when products of types are involved.</p>
<p>A better lemma to apply here is
<code class="docutils literal notranslate"><span class="pre">Continuous.dist</span> <span class="pre">{f</span> <span class="pre">g</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Y}</span> <span class="pre">:</span> <span class="pre">Continuous</span> <span class="pre">f</span> <span class="pre">&#8594;</span> <span class="pre">Continuous</span> <span class="pre">g</span> <span class="pre">&#8594;</span> <span class="pre">Continuous</span> <span class="pre">(fun</span> <span class="pre">x</span> <span class="pre">&#8614;</span> <span class="pre">dist</span> <span class="pre">(f</span> <span class="pre">x)</span> <span class="pre">(g</span> <span class="pre">x))</span></code>
which is nicer to Lean&#8217;s elaborator and also provides a shorter proof when directly providing a full
proof term, as can be seen from the following two new proofs of the above statement:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Continuous</span> <span class="k">fun</span> <span class="n">p</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#215;</span> <span class="n">X</span> <span class="bp">&#8614;</span> <span class="n">dist</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.1</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="n">Continuous.dist</span>
  <span class="n">exact</span> <span class="n">hf.comp</span> <span class="n">continuous_fst</span>
  <span class="n">exact</span> <span class="n">hf.comp</span> <span class="n">continuous_snd</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Continuous</span> <span class="k">fun</span> <span class="n">p</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#215;</span> <span class="n">X</span> <span class="bp">&#8614;</span> <span class="n">dist</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.1</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.2</span><span class="o">)</span> <span class="o">:=</span>
  <span class="o">(</span><span class="n">hf.comp</span> <span class="n">continuous_fst</span><span class="o">)</span><span class="bp">.</span><span class="n">dist</span> <span class="o">(</span><span class="n">hf.comp</span> <span class="n">continuous_snd</span><span class="o">)</span>
</pre></div>
</div>
<p>Note that, without the elaboration issue coming from composition, another way to compress
our proof would be to use <code class="docutils literal notranslate"><span class="pre">Continuous.prod_map</span></code> which is sometimes useful and gives
as an alternate proof term <code class="docutils literal notranslate"><span class="pre">continuous_dist.comp</span> <span class="pre">(hf.prod_map</span> <span class="pre">hf)</span></code> which even shorter to type.</p>
<p>Since it is sad to decide between a version which is better for elaboration and a version which is shorter
to type, let us wrap this discussion with a last bit of compression offered
by <code class="docutils literal notranslate"><span class="pre">Continuous.fst'</span></code> which allows to compress <code class="docutils literal notranslate"><span class="pre">hf.comp</span> <span class="pre">continuous_fst</span></code> to <code class="docutils literal notranslate"><span class="pre">hf.fst'</span></code> (and the same with <code class="docutils literal notranslate"><span class="pre">snd</span></code>)
and get our final proof, now bordering obfuscation.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Continuous</span> <span class="k">fun</span> <span class="n">p</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#215;</span> <span class="n">X</span> <span class="bp">&#8614;</span> <span class="n">dist</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.1</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="n">p.2</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">hf.fst&#39;.dist</span> <span class="n">hf.snd&#39;</span>
</pre></div>
</div>
<p>It&#8217;s your turn now to prove some continuity lemma. After trying the continuity tactic, you will need
<code class="docutils literal notranslate"><span class="pre">Continuous.add</span></code>, <code class="docutils literal notranslate"><span class="pre">continuous_pow</span></code> and <code class="docutils literal notranslate"><span class="pre">continuous_id</span></code> to do it by hand.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="k">fun</span> <span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#8614;</span> <span class="n">f</span> <span class="o">(</span><span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>So far we saw continuity as a global notion, but one can also define continuity at a point.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">ContinuousAt</span> <span class="n">f</span> <span class="n">a</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">&#948;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="o">{</span><span class="n">x</span><span class="o">},</span> <span class="n">dist</span> <span class="n">x</span> <span class="n">a</span> <span class="bp">&lt;</span> <span class="n">&#948;</span> <span class="bp">&#8594;</span> <span class="n">dist</span> <span class="o">(</span><span class="n">f</span> <span class="n">x</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="n">a</span><span class="o">)</span> <span class="bp">&lt;</span> <span class="n">&#949;</span> <span class="o">:=</span>
  <span class="n">Metric.continuousAt_iff</span>
</pre></div>
</div>
</section>
<section id="balls-open-sets-and-closed-sets">
<h3><span class="section-number">9.2.2. </span>Balls, open sets and closed sets<a class="headerlink" href="#balls-open-sets-and-closed-sets" title="Permalink to this heading">&#61633;</a></h3>
<p>Once we have a distance function, the most important geometric definitions are (open) balls and closed balls.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span> <span class="o">(</span><span class="n">r</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Metric.ball</span> <span class="n">a</span> <span class="n">r</span> <span class="bp">=</span> <span class="o">{</span> <span class="n">b</span> <span class="bp">|</span> <span class="n">dist</span> <span class="n">b</span> <span class="n">a</span> <span class="bp">&lt;</span> <span class="n">r</span> <span class="o">}</span> <span class="o">:=</span>
  <span class="n">rfl</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Metric.closedBall</span> <span class="n">a</span> <span class="n">r</span> <span class="bp">=</span> <span class="o">{</span> <span class="n">b</span> <span class="bp">|</span> <span class="n">dist</span> <span class="n">b</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">r</span> <span class="o">}</span> <span class="o">:=</span>
  <span class="n">rfl</span>
</pre></div>
</div>
<p>Note that <cite>r</cite> is any real number here, there is no sign restriction. Of course some statements do require a radius condition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">hr</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">r</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">Metric.ball</span> <span class="n">a</span> <span class="n">r</span> <span class="o">:=</span>
  <span class="n">Metric.mem_ball_self</span> <span class="n">hr</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">hr</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">r</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">Metric.closedBall</span> <span class="n">a</span> <span class="n">r</span> <span class="o">:=</span>
  <span class="n">Metric.mem_closedBall_self</span> <span class="n">hr</span>
</pre></div>
</div>
<p>Once we have balls, we can define open sets. They are actually defined in a more general setting covered in the next section,
but we have lemmas recasting the definition is terms of balls.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span> <span class="n">IsOpen</span> <span class="n">s</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="n">Metric.ball</span> <span class="n">x</span> <span class="n">&#949;</span> <span class="bp">&#8838;</span> <span class="n">s</span> <span class="o">:=</span>
  <span class="n">Metric.isOpen_iff</span>
</pre></div>
</div>
<p>Then closed sets are sets whose complement is open. Their important property is they are closed under limits. The closure of a set is the smallest closed set containing it.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">IsClosed</span> <span class="n">s</span> <span class="bp">&#8596;</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="n">s</span><span class="bp">&#7580;</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">isOpen_compl_iff.symm</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">IsClosed</span> <span class="n">s</span><span class="o">)</span> <span class="o">{</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hu</span> <span class="o">:</span> <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">a</span><span class="o">))</span>
    <span class="o">(</span><span class="n">hus</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">u</span> <span class="n">n</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">s</span> <span class="o">:=</span>
  <span class="n">hs.mem_of_tendsto</span> <span class="n">hu</span> <span class="o">(</span><span class="n">eventually_of_forall</span> <span class="n">hus</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">closure</span> <span class="n">s</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">b</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">Metric.ball</span> <span class="n">b</span> <span class="n">&#949;</span> <span class="o">:=</span>
  <span class="n">Metric.mem_closure_iff</span>
</pre></div>
</div>
<p>Do the next exercise without using <cite>mem_closure_iff_seq_limit</cite></p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hu</span> <span class="o">:</span> <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">a</span><span class="o">))</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">u</span> <span class="n">n</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">closure</span> <span class="n">s</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>Remember from the filters sections that neighborhood filters play a big role in Mathlib.
In the metric space context, the crucial point is that balls provide bases for those filters.
The main lemmas here are <code class="docutils literal notranslate"><span class="pre">Metric.nhds_basis_ball</span></code> and <code class="docutils literal notranslate"><span class="pre">Metric.nhds_basis_closedBall</span></code>
that claim this for open and closed balls with positive radius. The center point is an implicit
argument so we can invoke <code class="docutils literal notranslate"><span class="pre">Filter.HasBasis.mem_iff</span></code> as in the following example.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">s</span> <span class="bp">&#8712;</span> <span class="bp">&#120029;</span> <span class="n">x</span> <span class="bp">&#8596;</span> <span class="bp">&#8707;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="n">Metric.ball</span> <span class="n">x</span> <span class="n">&#949;</span> <span class="bp">&#8838;</span> <span class="n">s</span> <span class="o">:=</span>
  <span class="n">Metric.nhds_basis_ball.mem_iff</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">s</span> <span class="bp">&#8712;</span> <span class="bp">&#120029;</span> <span class="n">x</span> <span class="bp">&#8596;</span> <span class="bp">&#8707;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="n">Metric.closedBall</span> <span class="n">x</span> <span class="n">&#949;</span> <span class="bp">&#8838;</span> <span class="n">s</span> <span class="o">:=</span>
  <span class="n">Metric.nhds_basis_closedBall.mem_iff</span>
</pre></div>
</div>
</section>
<section id="compactness">
<h3><span class="section-number">9.2.3. </span>Compactness<a class="headerlink" href="#compactness" title="Permalink to this heading">&#61633;</a></h3>
<p>Compactness is an important topological notion. It distinguishes subsets of a metric space
that enjoy the same kind of properties as segments in reals compared to other intervals:</p>
<ul class="simple">
<li><p>Any sequence taking value in a compact set has a subsequence that converges in this set</p></li>
<li><p>Any continuous function on a nonempty compact set with values in real numbers is bounded and
achieves its bounds somewhere (this is called the extreme values theorem).</p></li>
<li><p>Compact sets are closed sets.</p></li>
</ul>
<p>Let us first check that the unit interval in reals is indeed a compact set, and then check the above
claims for compact sets in general metric spaces. In the second statement we only
need continuity on the given set so we will use <code class="docutils literal notranslate"><span class="pre">ContinuousOn</span></code> instead of <code class="docutils literal notranslate"><span class="pre">Continuous</span></code>, and
we will give separate statements for the minimum and the maximum. Of course all these results
are deduced from more general versions, some of which will be discussed in later sections.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="o">(</span><span class="n">Set.Icc</span> <span class="mi">0</span> <span class="mi">1</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">isCompact_Icc</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="n">s</span><span class="o">)</span> <span class="o">{</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hu</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">u</span> <span class="n">n</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#8707;</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">&#966;</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="n">StrictMono</span> <span class="n">&#966;</span> <span class="bp">&#8743;</span> <span class="n">Tendsto</span> <span class="o">(</span><span class="n">u</span> <span class="bp">&#8728;</span> <span class="n">&#966;</span><span class="o">)</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">a</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">hs.tendsto_subseq</span> <span class="n">hu</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="n">s</span><span class="o">)</span> <span class="o">(</span><span class="n">hs&#39;</span> <span class="o">:</span> <span class="n">s.Nonempty</span><span class="o">)</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">}</span>
      <span class="o">(</span><span class="n">hfs</span> <span class="o">:</span> <span class="n">ContinuousOn</span> <span class="n">f</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#8707;</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">y</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">&#8804;</span> <span class="n">f</span> <span class="n">y</span> <span class="o">:=</span>
  <span class="n">hs.exists_forall_le</span> <span class="n">hs&#39;</span> <span class="n">hfs</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="n">s</span><span class="o">)</span> <span class="o">(</span><span class="n">hs&#39;</span> <span class="o">:</span> <span class="n">s.Nonempty</span><span class="o">)</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span><span class="o">}</span>
      <span class="o">(</span><span class="n">hfs</span> <span class="o">:</span> <span class="n">ContinuousOn</span> <span class="n">f</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#8707;</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">y</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="n">f</span> <span class="n">y</span> <span class="bp">&#8804;</span> <span class="n">f</span> <span class="n">x</span> <span class="o">:=</span>
  <span class="n">hs.exists_forall_ge</span> <span class="n">hs&#39;</span> <span class="n">hfs</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span> <span class="n">IsClosed</span> <span class="n">s</span> <span class="o">:=</span>
  <span class="n">hs.isClosed</span>
</pre></div>
</div>
<p>We can also specify that a metric spaces is globally compact, using an extra <code class="docutils literal notranslate"><span class="pre">Prop</span></code>-valued type class:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">CompactSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="o">(</span><span class="n">univ</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">isCompact_univ</span>
</pre></div>
</div>
<p>In a compact metric space any closed set is compact, this is <code class="docutils literal notranslate"><span class="pre">IsClosed.isCompact</span></code>.</p>
</section>
<section id="uniformly-continuous-functions">
<h3><span class="section-number">9.2.4. </span>Uniformly continuous functions<a class="headerlink" href="#uniformly-continuous-functions" title="Permalink to this heading">&#61633;</a></h3>
<p>We now turn to uniformity notions on metric spaces : uniformly continuous functions, Cauchy sequences and completeness.
Again those are defined in a more general context but we have lemmas in the metric name space to access their elementary definitions.
We start with uniform continuity.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">{</span><span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">:</span>
    <span class="n">UniformContinuous</span> <span class="n">f</span> <span class="bp">&#8596;</span>
      <span class="bp">&#8704;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">&#948;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">X</span><span class="o">},</span> <span class="n">dist</span> <span class="n">a</span> <span class="n">b</span> <span class="bp">&lt;</span> <span class="n">&#948;</span> <span class="bp">&#8594;</span> <span class="n">dist</span> <span class="o">(</span><span class="n">f</span> <span class="n">a</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="n">b</span><span class="o">)</span> <span class="bp">&lt;</span> <span class="n">&#949;</span> <span class="o">:=</span>
  <span class="n">Metric.uniformContinuous_iff</span>
</pre></div>
</div>
<p>In order to practice manipulating all those definitions, we will prove that continuous
functions from a compact metric space to a metric space are uniformly continuous
(we will see a more general version in a later section).</p>
<p>We will first give an informal sketch. Let <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Y</span></code> be a continuous function from
a compact metric space to a metric space.
We fix <code class="docutils literal notranslate"><span class="pre">&#949;</span> <span class="pre">&gt;</span> <span class="pre">0</span></code> and start looking for some <code class="docutils literal notranslate"><span class="pre">&#948;</span></code>.</p>
<p>Let <code class="docutils literal notranslate"><span class="pre">&#966;</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#215;</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span> <span class="pre">:=</span> <span class="pre">fun</span> <span class="pre">p</span> <span class="pre">&#8614;</span> <span class="pre">dist</span> <span class="pre">(f</span> <span class="pre">p.1)</span> <span class="pre">(f</span> <span class="pre">p.2)</span></code> and let <code class="docutils literal notranslate"><span class="pre">K</span> <span class="pre">:=</span> <span class="pre">{</span> <span class="pre">p</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#215;</span> <span class="pre">X</span> <span class="pre">|</span> <span class="pre">&#949;</span> <span class="pre">&#8804;</span> <span class="pre">&#966;</span> <span class="pre">p</span> <span class="pre">}</span></code>.
Observe <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> is continuous since <code class="docutils literal notranslate"><span class="pre">f</span></code> and distance are continuous.
And <code class="docutils literal notranslate"><span class="pre">K</span></code> is clearly closed (use <code class="docutils literal notranslate"><span class="pre">isClosed_le</span></code>) hence compact since <code class="docutils literal notranslate"><span class="pre">X</span></code> is compact.</p>
<p>Then we discuss two possibilities using <code class="docutils literal notranslate"><span class="pre">eq_empty_or_nonempty</span></code>.
If <code class="docutils literal notranslate"><span class="pre">K</span></code> is empty then we are clearly done (we can set <code class="docutils literal notranslate"><span class="pre">&#948;</span> <span class="pre">=</span> <span class="pre">1</span></code> for instance).
So let&#8217;s assume <code class="docutils literal notranslate"><span class="pre">K</span></code> is not empty, and use the extreme value theorem to choose <code class="docutils literal notranslate"><span class="pre">(x&#8320;,</span> <span class="pre">x&#8321;)</span></code> attaining the infimum
of the distance function on <code class="docutils literal notranslate"><span class="pre">K</span></code>. We can then set <code class="docutils literal notranslate"><span class="pre">&#948;</span> <span class="pre">=</span> <span class="pre">dist</span> <span class="pre">x&#8320;</span> <span class="pre">x&#8321;</span></code> and check everything works.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">X</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">CompactSpace</span> <span class="n">X</span><span class="o">]</span>
      <span class="o">{</span><span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">MetricSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span>
    <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span> <span class="n">UniformContinuous</span> <span class="n">f</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="completeness">
<h3><span class="section-number">9.2.5. </span>Completeness<a class="headerlink" href="#completeness" title="Permalink to this heading">&#61633;</a></h3>
<p>A Cauchy sequence in a metric space is a sequence whose terms get closer and closer to each other.
There are a couple of equivalent ways to state that idea.
In particular converging sequences are Cauchy. The converse is true only in so-called <em>complete</em>
spaces.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">CauchySeq</span> <span class="n">u</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">N</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">m</span> <span class="bp">&#8805;</span> <span class="n">N</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">n</span> <span class="bp">&#8805;</span> <span class="n">N</span><span class="o">,</span> <span class="n">dist</span> <span class="o">(</span><span class="n">u</span> <span class="n">m</span><span class="o">)</span> <span class="o">(</span><span class="n">u</span> <span class="n">n</span><span class="o">)</span> <span class="bp">&lt;</span> <span class="n">&#949;</span> <span class="o">:=</span>
  <span class="n">Metric.cauchySeq_iff</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">CauchySeq</span> <span class="n">u</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">&#949;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">N</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">n</span> <span class="bp">&#8805;</span> <span class="n">N</span><span class="o">,</span> <span class="n">dist</span> <span class="o">(</span><span class="n">u</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">u</span> <span class="n">N</span><span class="o">)</span> <span class="bp">&lt;</span> <span class="n">&#949;</span> <span class="o">:=</span>
  <span class="n">Metric.cauchySeq_iff&#39;</span>

<span class="kd">example</span> <span class="o">[</span><span class="n">CompleteSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">(</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">hu</span> <span class="o">:</span> <span class="n">CauchySeq</span> <span class="n">u</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#8707;</span> <span class="n">x</span><span class="o">,</span> <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">cauchySeq_tendsto_of_complete</span> <span class="n">hu</span>
</pre></div>
</div>
<p>We&#8217;ll practice using this definition by proving a convenient criterion which is a special case of a
criterion appearing in Mathlib. This is also a good opportunity to practice using big sums in
a geometric context. In addition to the explanations from the filters section, you will probably need
<code class="docutils literal notranslate"><span class="pre">tendsto_pow_atTop_nhds_0_of_lt_1</span></code>, <code class="docutils literal notranslate"><span class="pre">Tendsto.mul</span></code> and <code class="docutils literal notranslate"><span class="pre">dist_le_range_sum_dist</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">cauchySeq_of_le_geometric_two&#39;</span> <span class="o">{</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span>
    <span class="o">(</span><span class="n">hu</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="n">dist</span> <span class="o">(</span><span class="n">u</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">u</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">))</span> <span class="bp">&#8804;</span> <span class="o">(</span><span class="mi">1</span> <span class="bp">/</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">^</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">CauchySeq</span> <span class="n">u</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">Metric.cauchySeq_iff&#39;</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">&#949;</span> <span class="n">&#949;_pos</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">N</span><span class="o">,</span> <span class="n">hN</span><span class="o">&#10217;</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">N</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="mi">1</span> <span class="bp">/</span> <span class="mi">2</span> <span class="bp">^</span> <span class="n">N</span> <span class="bp">*</span> <span class="mi">2</span> <span class="bp">&lt;</span> <span class="n">&#949;</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="n">use</span> <span class="n">N</span>
  <span class="n">intro</span> <span class="n">n</span> <span class="n">hn</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">rfl</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">=</span> <span class="n">N</span> <span class="bp">+</span> <span class="n">k</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">le_iff_exists_add.mp</span> <span class="n">hn</span>
  <span class="k">calc</span>
    <span class="n">dist</span> <span class="o">(</span><span class="n">u</span> <span class="o">(</span><span class="n">N</span> <span class="bp">+</span> <span class="n">k</span><span class="o">))</span> <span class="o">(</span><span class="n">u</span> <span class="n">N</span><span class="o">)</span> <span class="bp">=</span> <span class="n">dist</span> <span class="o">(</span><span class="n">u</span> <span class="o">(</span><span class="n">N</span> <span class="bp">+</span> <span class="mi">0</span><span class="o">))</span> <span class="o">(</span><span class="n">u</span> <span class="o">(</span><span class="n">N</span> <span class="bp">+</span> <span class="n">k</span><span class="o">))</span> <span class="o">:=</span> <span class="gr">sorry</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="bp">&#8721;</span> <span class="n">i</span> <span class="k">in</span> <span class="n">range</span> <span class="n">k</span><span class="o">,</span> <span class="n">dist</span> <span class="o">(</span><span class="n">u</span> <span class="o">(</span><span class="n">N</span> <span class="bp">+</span> <span class="n">i</span><span class="o">))</span> <span class="o">(</span><span class="n">u</span> <span class="o">(</span><span class="n">N</span> <span class="bp">+</span> <span class="o">(</span><span class="n">i</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)))</span> <span class="o">:=</span> <span class="gr">sorry</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="bp">&#8721;</span> <span class="n">i</span> <span class="k">in</span> <span class="n">range</span> <span class="n">k</span><span class="o">,</span> <span class="o">(</span><span class="mi">1</span> <span class="bp">/</span> <span class="mi">2</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">^</span> <span class="o">(</span><span class="n">N</span> <span class="bp">+</span> <span class="n">i</span><span class="o">)</span> <span class="o">:=</span> <span class="gr">sorry</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">1</span> <span class="bp">/</span> <span class="mi">2</span> <span class="bp">^</span> <span class="n">N</span> <span class="bp">*</span> <span class="bp">&#8721;</span> <span class="n">i</span> <span class="k">in</span> <span class="n">range</span> <span class="n">k</span><span class="o">,</span> <span class="o">(</span><span class="mi">1</span> <span class="bp">/</span> <span class="mi">2</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">^</span> <span class="n">i</span> <span class="o">:=</span> <span class="gr">sorry</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="mi">1</span> <span class="bp">/</span> <span class="mi">2</span> <span class="bp">^</span> <span class="n">N</span> <span class="bp">*</span> <span class="mi">2</span> <span class="o">:=</span> <span class="gr">sorry</span>
    <span class="n">_</span> <span class="bp">&lt;</span> <span class="n">&#949;</span> <span class="o">:=</span> <span class="gr">sorry</span>
</pre></div>
</div>
<p>We are ready for the final boss of this section: Baire&#8217;s theorem for complete metric spaces!
The proof skeleton below shows interesting techniques. It uses the <code class="docutils literal notranslate"><span class="pre">choose</span></code> tactic in its exclamation
mark variant (you should experiment with removing this exclamation mark) and it shows how to
define something inductively in the middle of a proof using <code class="docutils literal notranslate"><span class="pre">Nat.rec_on</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span> <span class="n">Metric</span>

<span class="kd">example</span> <span class="o">[</span><span class="n">CompleteSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">Set</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">ho</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="n">f</span> <span class="n">n</span><span class="o">))</span> <span class="o">(</span><span class="n">hd</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">Dense</span> <span class="o">(</span><span class="n">f</span> <span class="n">n</span><span class="o">))</span> <span class="o">:</span>
    <span class="n">Dense</span> <span class="o">(</span><span class="bp">&#8898;</span> <span class="n">n</span><span class="o">,</span> <span class="n">f</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">let</span> <span class="n">B</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">n</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="mi">1</span> <span class="bp">/</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">^</span> <span class="n">n</span>
  <span class="k">have</span> <span class="n">Bpos</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">B</span> <span class="n">n</span>
  <span class="gr">sorry</span>
  <span class="c">/-</span><span class="cm"> Translate the density assumption into two functions `center` and `radius` associating</span>
<span class="cm">    to any n, x, &#948;, &#948;pos a center and a positive radius such that</span>
<span class="cm">    `closedBall center radius` is included both in `f n` and in `closedBall x &#948;`.</span>
<span class="cm">    We can also require `radius &#8804; (1/2)^(n+1)`, to ensure we get a Cauchy sequence later. -/</span>
  <span class="k">have</span> <span class="o">:</span>
    <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">),</span>
      <span class="bp">&#8704;</span> <span class="n">&#948;</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">y</span> <span class="o">:</span> <span class="n">X</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">r</span> <span class="bp">&gt;</span> <span class="mi">0</span><span class="o">,</span> <span class="n">r</span> <span class="bp">&#8804;</span> <span class="n">B</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">&#8743;</span> <span class="n">closedBall</span> <span class="n">y</span> <span class="n">r</span> <span class="bp">&#8838;</span> <span class="n">closedBall</span> <span class="n">x</span> <span class="n">&#948;</span> <span class="bp">&#8745;</span> <span class="n">f</span> <span class="n">n</span> <span class="o">:=</span>
    <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="n">choose</span><span class="bp">!</span> <span class="n">center</span> <span class="n">radius</span> <span class="n">Hpos</span> <span class="n">HB</span> <span class="n">Hball</span> <span class="n">using</span> <span class="n">this</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">mem_closure_iff_nhds_basis</span> <span class="n">nhds_basis_closedBall</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">&#949;</span> <span class="n">&#949;pos</span>
  <span class="c">/-</span><span class="cm"> `&#949;` is positive. We have to find a point in the ball of radius `&#949;` around `x`</span>
<span class="cm">    belonging to all `f n`. For this, we construct inductively a sequence</span>
<span class="cm">    `F n = (c n, r n)` such that the closed ball `closedBall (c n) (r n)` is included</span>
<span class="cm">    in the previous ball and in `f n`, and such that `r n` is small enough to ensure</span>
<span class="cm">    that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs</span>
<span class="cm">    to all the `f n`. -/</span>
  <span class="k">let</span> <span class="n">F</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">n</span> <span class="bp">&#8614;</span>
    <span class="n">Nat.recOn</span> <span class="n">n</span> <span class="o">(</span><span class="n">Prod.mk</span> <span class="n">x</span> <span class="o">(</span><span class="n">min</span> <span class="n">&#949;</span> <span class="o">(</span><span class="n">B</span> <span class="mi">0</span><span class="o">)))</span>
      <span class="k">fun</span> <span class="n">n</span> <span class="n">p</span> <span class="bp">&#8614;</span> <span class="n">Prod.mk</span> <span class="o">(</span><span class="n">center</span> <span class="n">n</span> <span class="n">p.1</span> <span class="n">p.2</span><span class="o">)</span> <span class="o">(</span><span class="n">radius</span> <span class="n">n</span> <span class="n">p.1</span> <span class="n">p.2</span><span class="o">)</span>
  <span class="k">let</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">n</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">F</span> <span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="mi">1</span>
  <span class="k">let</span> <span class="n">r</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="k">fun</span> <span class="n">n</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">F</span> <span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="mi">2</span>
  <span class="k">have</span> <span class="n">rpos</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">r</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="k">have</span> <span class="n">rB</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">r</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="n">B</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="k">have</span> <span class="n">incl</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">closedBall</span> <span class="o">(</span><span class="n">c</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">))</span> <span class="o">(</span><span class="n">r</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">))</span> <span class="bp">&#8838;</span> <span class="n">closedBall</span> <span class="o">(</span><span class="n">c</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">r</span> <span class="n">n</span><span class="o">)</span> <span class="bp">&#8745;</span> <span class="n">f</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
    <span class="gr">sorry</span>
  <span class="k">have</span> <span class="n">cdist</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">dist</span> <span class="o">(</span><span class="n">c</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">c</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">))</span> <span class="bp">&#8804;</span> <span class="n">B</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="k">have</span> <span class="o">:</span> <span class="n">CauchySeq</span> <span class="n">c</span> <span class="o">:=</span> <span class="n">cauchySeq_of_le_geometric_two&#39;</span> <span class="n">cdist</span>
  <span class="c1">-- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.</span>
  <span class="n">rcases</span> <span class="n">cauchySeq_tendsto_of_complete</span> <span class="n">this</span> <span class="k">with</span> <span class="o">&#10216;</span><span class="n">y</span><span class="o">,</span> <span class="n">ylim</span><span class="o">&#10217;</span>
  <span class="c1">-- this point `y` will be the desired point. We will check that it belongs to all</span>
  <span class="c1">-- `f n` and to `ball x &#949;`.</span>
  <span class="n">use</span> <span class="n">y</span>
  <span class="k">have</span> <span class="n">I</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">m</span> <span class="bp">&#8805;</span> <span class="n">n</span><span class="o">,</span> <span class="n">closedBall</span> <span class="o">(</span><span class="n">c</span> <span class="n">m</span><span class="o">)</span> <span class="o">(</span><span class="n">r</span> <span class="n">m</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="n">closedBall</span> <span class="o">(</span><span class="n">c</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">r</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="k">have</span> <span class="n">yball</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">y</span> <span class="bp">&#8712;</span> <span class="n">closedBall</span> <span class="o">(</span><span class="n">c</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">r</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
</section>
<section id="topological-spaces">
<span id="index-4"></span><span id="id4"></span><h2><span class="section-number">9.3. </span>Topological spaces<a class="headerlink" href="#topological-spaces" title="Permalink to this heading">&#61633;</a></h2>
<section id="fundamentals">
<h3><span class="section-number">9.3.1. </span>Fundamentals<a class="headerlink" href="#fundamentals" title="Permalink to this heading">&#61633;</a></h3>
<p>We now go up in generality and introduce topological spaces. We will review the two main ways to define
topological spaces and then explain how the category of topological spaces is much better behaved than
the category of metric spaces. Note that we won&#8217;t be using Mathlib category theory here, only having
a somewhat categorical point of view.</p>
<p>The first way to think about the transition from metric spaces to topological spaces is that we only
remember the notion of open sets (or equivalently the notion of closed sets). From this point of view,
a topological space is a type equipped with a collection of sets that are called open sets. This collection
has to satisfy a number of axioms presented below (this collection is slightly redundant but we will ignore that).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="kd">variable</span> <span class="o">{</span><span class="n">X</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="n">univ</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">isOpen_univ</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="bp">&#8709;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">isOpen_empty</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">&#953;</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">&#953;</span> <span class="bp">&#8594;</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">i</span><span class="o">,</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="n">s</span> <span class="n">i</span><span class="o">))</span> <span class="o">:</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="bp">&#8899;</span> <span class="n">i</span><span class="o">,</span> <span class="n">s</span> <span class="n">i</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">isOpen_iUnion</span> <span class="n">hs</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">&#953;</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">Fintype</span> <span class="n">&#953;</span><span class="o">]</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">&#953;</span> <span class="bp">&#8594;</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">i</span><span class="o">,</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="n">s</span> <span class="n">i</span><span class="o">))</span> <span class="o">:</span>
    <span class="n">IsOpen</span> <span class="o">(</span><span class="bp">&#8898;</span> <span class="n">i</span><span class="o">,</span> <span class="n">s</span> <span class="n">i</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">isOpen_iInter_of_finite</span> <span class="n">hs</span>
</pre></div>
</div>
<p>Closed sets are then defined as sets whose complement  is open. A function between topological spaces
is (globally) continuous if all preimages of open sets are open.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span> <span class="o">{</span><span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">Y</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">s</span><span class="o">,</span> <span class="n">IsOpen</span> <span class="n">s</span> <span class="bp">&#8594;</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="n">f</span> <span class="bp">&#8315;&#185;&#39;</span> <span class="n">s</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">continuous_def</span>
</pre></div>
</div>
<p>With this definition we already see that, compared to metric spaces, topological spaces only remember
enough information to talk about continuous functions: two topological structures on a type are
the same if and only if they have the same continuous functions (indeed the identity function will
be continuous in both direction if and only if the two structures have the same open sets).</p>
<p>However as soon as we move on to continuity at a point we see the limitations of the approach based
on open sets. In Mathlib we frequently think of topological spaces as types equipped
with a neighborhood filter <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x</span></code> attached to each point <code class="docutils literal notranslate"><span class="pre">x</span></code> (the corresponding function
<code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">X</span></code> satisfies certain conditions explained further down). Remember from the filters section that
these gadgets play two related roles. First <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x</span></code> is seen as the generalized set of points of <code class="docutils literal notranslate"><span class="pre">X</span></code>
that are close to <code class="docutils literal notranslate"><span class="pre">x</span></code>. And then it is seen as giving a way to say, for any predicate <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Prop</span></code>,
that this predicate holds for points that are close enough to <code class="docutils literal notranslate"><span class="pre">x</span></code>. Let us state
that <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Y</span></code> is continuous at <code class="docutils literal notranslate"><span class="pre">x</span></code>. The purely filtery way is to say that the direct image under
<code class="docutils literal notranslate"><span class="pre">f</span></code> of the generalized set of points that are close to <code class="docutils literal notranslate"><span class="pre">x</span></code> is contained in the generalized set of
points that are close to <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code>. Recall this is spelled either <code class="docutils literal notranslate"><span class="pre">map</span> <span class="pre">f</span> <span class="pre">(&#120029;</span> <span class="pre">x)</span> <span class="pre">&#8804;</span> <span class="pre">&#120029;</span> <span class="pre">(f</span> <span class="pre">x)</span></code>
or <code class="docutils literal notranslate"><span class="pre">Tendsto</span> <span class="pre">f</span> <span class="pre">(&#120029;</span> <span class="pre">x)</span> <span class="pre">(&#120029;</span> <span class="pre">(f</span> <span class="pre">x))</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">ContinuousAt</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">&#8596;</span> <span class="n">map</span> <span class="n">f</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x</span><span class="o">)</span> <span class="bp">&#8804;</span> <span class="bp">&#120029;</span> <span class="o">(</span><span class="n">f</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">Iff.rfl</span>
</pre></div>
</div>
<p>One can also spell it using both neighborhoods seen as ordinary sets and a neighborhood filter
seen as a generalized set: &#8220;for any neighborhood <code class="docutils literal notranslate"><span class="pre">U</span></code> of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code>, all points close to <code class="docutils literal notranslate"><span class="pre">x</span></code>
are sent to <code class="docutils literal notranslate"><span class="pre">U</span></code>&#8221;. Note that the proof is again <code class="docutils literal notranslate"><span class="pre">iff.rfl</span></code>, this point of view is definitionally
equivalent to the previous one.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">ContinuousAt</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">U</span> <span class="bp">&#8712;</span> <span class="bp">&#120029;</span> <span class="o">(</span><span class="n">f</span> <span class="n">x</span><span class="o">),</span> <span class="bp">&#8704;&#7584;</span> <span class="n">x</span> <span class="k">in</span> <span class="bp">&#120029;</span> <span class="n">x</span><span class="o">,</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">U</span> <span class="o">:=</span>
  <span class="n">Iff.rfl</span>
</pre></div>
</div>
<p>We now explain how to go from one point of view to the other. In terms of open sets, we can
simply define members of <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x</span></code> as sets that contain an open set containing <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">s</span> <span class="bp">&#8712;</span> <span class="bp">&#120029;</span> <span class="n">x</span> <span class="bp">&#8596;</span> <span class="bp">&#8707;</span> <span class="n">t</span><span class="o">,</span> <span class="n">t</span> <span class="bp">&#8838;</span> <span class="n">s</span> <span class="bp">&#8743;</span> <span class="n">IsOpen</span> <span class="n">t</span> <span class="bp">&#8743;</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">t</span> <span class="o">:=</span>
  <span class="n">mem_nhds_iff</span>
</pre></div>
</div>
<p>To go in the other direction we need to discuss the condition that <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">X</span></code> must satisfy
in order to be the neighborhood function of a topology.</p>
<p>The first constraint is that <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x</span></code>, seen as a generalized set, contains the set <code class="docutils literal notranslate"><span class="pre">{x}</span></code> seen as the generalized set
<code class="docutils literal notranslate"><span class="pre">pure</span> <span class="pre">x</span></code> (explaining this weird name would be too much of a digression, so we simply accept it for now).
Another way to say it is that if a predicate holds for points close to <code class="docutils literal notranslate"><span class="pre">x</span></code> then it holds at <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span> <span class="n">pure</span> <span class="n">x</span> <span class="bp">&#8804;</span> <span class="bp">&#120029;</span> <span class="n">x</span> <span class="o">:=</span>
  <span class="n">pure_le_nhds</span> <span class="n">x</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">P</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">y</span> <span class="k">in</span> <span class="bp">&#120029;</span> <span class="n">x</span><span class="o">,</span> <span class="n">P</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">P</span> <span class="n">x</span> <span class="o">:=</span>
  <span class="n">h.self_of_nhds</span>
</pre></div>
</div>
<p>Then a more subtle requirement is that, for any predicate <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Prop</span></code> and any <code class="docutils literal notranslate"><span class="pre">x</span></code>, if <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">y</span></code> holds for <code class="docutils literal notranslate"><span class="pre">y</span></code> close
to <code class="docutils literal notranslate"><span class="pre">x</span></code> then for <code class="docutils literal notranslate"><span class="pre">y</span></code> close to <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">z</span></code> close to <code class="docutils literal notranslate"><span class="pre">y</span></code>, <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">z</span></code> holds. More precisely we have:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">P</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span><span class="o">}</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">y</span> <span class="k">in</span> <span class="bp">&#120029;</span> <span class="n">x</span><span class="o">,</span> <span class="n">P</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8704;&#7584;</span> <span class="n">y</span> <span class="k">in</span> <span class="bp">&#120029;</span> <span class="n">x</span><span class="o">,</span> <span class="bp">&#8704;&#7584;</span> <span class="n">z</span> <span class="k">in</span> <span class="bp">&#120029;</span> <span class="n">y</span><span class="o">,</span> <span class="n">P</span> <span class="n">z</span> <span class="o">:=</span>
  <span class="n">eventually_eventually_nhds.mpr</span> <span class="n">h</span>
</pre></div>
</div>
<p>Those two results characterize the functions <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">X</span></code> that are neighborhood functions for a topological space
structure on <code class="docutils literal notranslate"><span class="pre">X</span></code>. There is a still a function <code class="docutils literal notranslate"><span class="pre">TopologicalSpace.mkOfNhds</span> <span class="pre">:</span> <span class="pre">(X</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">X)</span> <span class="pre">&#8594;</span> <span class="pre">TopologicalSpace</span> <span class="pre">X</span></code>
but it will give back its input as a neighborhood function only if it satisfies the above two constraints.
More precisely we have a lemma <code class="docutils literal notranslate"><span class="pre">TopologicalSpace.nhds_mkOfNhds</span></code> saying that in a different way and our
next exercise deduces this different way from how we stated it above.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">&#945;</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">Filter</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">(</span><span class="n">H&#8320;</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span><span class="o">,</span> <span class="n">pure</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">n</span> <span class="n">a</span><span class="o">)</span>
    <span class="o">(</span><span class="n">H</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">p</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span><span class="o">,</span> <span class="o">(</span><span class="bp">&#8704;&#7584;</span> <span class="n">x</span> <span class="k">in</span> <span class="n">n</span> <span class="n">a</span><span class="o">,</span> <span class="n">p</span> <span class="n">x</span><span class="o">)</span> <span class="bp">&#8594;</span> <span class="bp">&#8704;&#7584;</span> <span class="n">y</span> <span class="k">in</span> <span class="n">n</span> <span class="n">a</span><span class="o">,</span> <span class="bp">&#8704;&#7584;</span> <span class="n">x</span> <span class="k">in</span> <span class="n">n</span> <span class="n">y</span><span class="o">,</span> <span class="n">p</span> <span class="n">x</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#8704;</span> <span class="n">a</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">s</span> <span class="bp">&#8712;</span> <span class="n">n</span> <span class="n">a</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">t</span> <span class="bp">&#8712;</span> <span class="n">n</span> <span class="n">a</span><span class="o">,</span> <span class="n">t</span> <span class="bp">&#8838;</span> <span class="n">s</span> <span class="bp">&#8743;</span> <span class="bp">&#8704;</span> <span class="n">a&#39;</span> <span class="bp">&#8712;</span> <span class="n">t</span><span class="o">,</span> <span class="n">s</span> <span class="bp">&#8712;</span> <span class="n">n</span> <span class="n">a&#39;</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>Note that <code class="docutils literal notranslate"><span class="pre">TopologicalSpace.mkOfNhds</span></code> is not so frequently used, but it still good to know in what
precise sense the neighborhood filters is all there is in a topological space structure.</p>
<p>The next thing to know in order to efficiently use topological spaces in Mathlib is that we use a lot
of formal properties of <code class="docutils literal notranslate"><span class="pre">TopologicalSpace</span> <span class="pre">:</span> <span class="pre">Type</span> <span class="pre">u</span> <span class="pre">&#8594;</span> <span class="pre">Type</span> <span class="pre">u</span></code>. From a purely mathematical point of view,
those formal properties are a very clean way to explain how topological spaces solve issues that metric spaces
have. From this point of view, the issues solved by topological spaces is that metric spaces enjoy very
little functoriality, and have very bad categorical properties in general. This comes on top of the fact
already discussed that metric spaces contain a lot of geometrical information that is not topologically relevant.</p>
<p>Let us focus on functoriality first. A metric space structure can be induced on a subset or,
equivalently, it can be pulled back by an injective map. But that&#8217;s pretty much everything.
They cannot be pulled back by general map or pushed forward, even by surjective maps.</p>
<p>In particular there is no sensible distance to put on a quotient of a metric space or on an uncountable
products of metric spaces. Consider for instance the type <code class="docutils literal notranslate"><span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code>, seen as
a product of copies of <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> indexed by <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>. We would like to say that pointwise convergence of
sequences of functions is a respectable notion of convergence. But there is no distance on
<code class="docutils literal notranslate"><span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> that gives this notion of convergence. Relatedly, there is no distance ensuring that
a map <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">(&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;)</span></code> is continuous if and only <code class="docutils literal notranslate"><span class="pre">fun</span> <span class="pre">x</span> <span class="pre">&#8614;</span> <span class="pre">f</span> <span class="pre">x</span> <span class="pre">t</span></code> is continuous for every <code class="docutils literal notranslate"><span class="pre">t</span> <span class="pre">:</span> <span class="pre">&#8477;</span></code>.</p>
<p>We now review the data used to solve all those issues. First we can use any map <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Y</span></code> to
push or pull topologies from one side to the other. Those two operations form a Galois connection.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">TopologicalSpace</span> <span class="n">Y</span> <span class="o">:=</span>
  <span class="n">TopologicalSpace.coinduced</span> <span class="n">f</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">TopologicalSpace</span> <span class="n">X</span> <span class="o">:=</span>
  <span class="n">TopologicalSpace.induced</span> <span class="n">f</span>

<span class="kd">example</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">T_X</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">T_Y</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">TopologicalSpace.coinduced</span> <span class="n">f</span> <span class="n">T_X</span> <span class="bp">&#8804;</span> <span class="n">T_Y</span> <span class="bp">&#8596;</span> <span class="n">T_X</span> <span class="bp">&#8804;</span> <span class="n">TopologicalSpace.induced</span> <span class="n">f</span> <span class="n">T_Y</span> <span class="o">:=</span>
  <span class="n">coinduced_le_iff_le_induced</span>
</pre></div>
</div>
<p>Those operations are compactible with composition of functions.
As usual, pushing forward is covariant and pulling back is contravariant, see <code class="docutils literal notranslate"><span class="pre">coinduced_compose</span></code> and <code class="docutils literal notranslate"><span class="pre">induced_compose</span></code>.
On paper we will use notations <span class="math notranslate nohighlight">\(f_*T\)</span> for <code class="docutils literal notranslate"><span class="pre">TopologicalSpace.coinduced</span> <span class="pre">f</span> <span class="pre">T</span></code> and
<span class="math notranslate nohighlight">\(f^*T\)</span> for <code class="docutils literal notranslate"><span class="pre">TopologicalSpace.induced</span> <span class="pre">f</span> <span class="pre">T</span></code>.</p>
<p>Then the next big piece is a complete lattice structure on <code class="docutils literal notranslate"><span class="pre">TopologicalSpace</span> <span class="pre">X</span></code>
for any given structure. If you think of topologies are being primarily the data of open sets then you expect
the order relation on <code class="docutils literal notranslate"><span class="pre">TopologicalSpace</span> <span class="pre">X</span></code> to come from <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">(Set</span> <span class="pre">X)</span></code>, ie you expect <code class="docutils literal notranslate"><span class="pre">t</span> <span class="pre">&#8804;</span> <span class="pre">t'</span></code>
if a set <code class="docutils literal notranslate"><span class="pre">u</span></code> is open for <code class="docutils literal notranslate"><span class="pre">t'</span></code> as soon as it is open for <code class="docutils literal notranslate"><span class="pre">t</span></code>. However we already know that Mathlib focuses
on neighborhoods more than open sets so, for any <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">:</span> <span class="pre">X</span></code> we want the map from topological spaces to neighborhoods
<code class="docutils literal notranslate"><span class="pre">fun</span> <span class="pre">T</span> <span class="pre">:</span> <span class="pre">TopologicalSpace</span> <span class="pre">X</span> <span class="pre">&#8614;</span> <span class="pre">&#64;nhds</span> <span class="pre">X</span> <span class="pre">T</span> <span class="pre">x</span></code> to be order preserving.
And we know the order relation on <code class="docutils literal notranslate"><span class="pre">Filter</span> <span class="pre">X</span></code> is designed to ensure an order
preserving <code class="docutils literal notranslate"><span class="pre">principal</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">X</span> <span class="pre">&#8594;</span> <span class="pre">Filter</span> <span class="pre">X</span></code>, allowing to see filters as generalized sets.
So the order relation we do use on  <code class="docutils literal notranslate"><span class="pre">TopologicalSpace</span> <span class="pre">X</span></code> is opposite to the one coming from <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">(Set</span> <span class="pre">X)</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">T</span> <span class="n">T&#39;</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">T</span> <span class="bp">&#8804;</span> <span class="n">T&#39;</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">s</span><span class="o">,</span> <span class="n">T&#39;.IsOpen</span> <span class="n">s</span> <span class="bp">&#8594;</span> <span class="n">T.IsOpen</span> <span class="n">s</span> <span class="o">:=</span>
  <span class="n">Iff.rfl</span>
</pre></div>
</div>
<p>Now we can recover continuity by combining the push-forward (or pull-back) operation with the order relation.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">T_X</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">T_Y</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Continuous</span> <span class="n">f</span> <span class="bp">&#8596;</span> <span class="n">TopologicalSpace.coinduced</span> <span class="n">f</span> <span class="n">T_X</span> <span class="bp">&#8804;</span> <span class="n">T_Y</span> <span class="o">:=</span>
  <span class="n">continuous_iff_coinduced_le</span>
</pre></div>
</div>
<p>With this definition and the compatibility of push-forward and composition, we
get for free the universal property that, for any topological space <span class="math notranslate nohighlight">\(Z\)</span>,
a function <span class="math notranslate nohighlight">\(g : Y &#8594; Z\)</span> is continuous for the topology <span class="math notranslate nohighlight">\(f_*T_X\)</span> if and only if
<span class="math notranslate nohighlight">\(g &#8728; f\)</span> is continuous.</p>
<div class="math notranslate nohighlight">
\[\begin{split}g \text{ continuous } &amp;&#8660; g_*(f_*T_X) &#8804; T_Z \\
&amp;&#8660; (g &#8728; f)_* T_X &#8804; T_Z \\
&amp;&#8660; g &#8728; f \text{ continuous}\end{split}\]</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">Z</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">T_X</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">T_Z</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="n">Z</span><span class="o">)</span>
      <span class="o">(</span><span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">Z</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">@</span><span class="n">Continuous</span> <span class="n">Y</span> <span class="n">Z</span> <span class="o">(</span><span class="n">TopologicalSpace.coinduced</span> <span class="n">f</span> <span class="n">T_X</span><span class="o">)</span> <span class="n">T_Z</span> <span class="n">g</span> <span class="bp">&#8596;</span>
      <span class="bp">@</span><span class="n">Continuous</span> <span class="n">X</span> <span class="n">Z</span> <span class="n">T_X</span> <span class="n">T_Z</span> <span class="o">(</span><span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">continuous_iff_coinduced_le</span><span class="o">,</span> <span class="n">coinduced_compose</span><span class="o">,</span> <span class="n">continuous_iff_coinduced_le</span><span class="o">]</span>
</pre></div>
</div>
<p>So we already get quotient topologies (using the projection map as <code class="docutils literal notranslate"><span class="pre">f</span></code>). This wasn&#8217;t using that
<code class="docutils literal notranslate"><span class="pre">TopologicalSpace</span> <span class="pre">X</span></code> is a complete lattice for all <code class="docutils literal notranslate"><span class="pre">X</span></code>. Let&#8217;s now see how all this structure
proves the existence of the product topology by abstract non-sense.
We considered the case of <code class="docutils literal notranslate"><span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> above, but let&#8217;s now consider the general case of <code class="docutils literal notranslate"><span class="pre">&#928;</span> <span class="pre">i,</span> <span class="pre">X</span> <span class="pre">i</span></code> for
some <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">:</span> <span class="pre">Type*</span></code> and <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">:</span> <span class="pre">&#953;</span> <span class="pre">&#8594;</span> <span class="pre">Type*</span></code>. We want, for any topological space <code class="docutils literal notranslate"><span class="pre">Z</span></code> and any function
<code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">Z</span> <span class="pre">&#8594;</span> <span class="pre">&#928;</span> <span class="pre">i,</span> <span class="pre">X</span> <span class="pre">i</span></code>, that <code class="docutils literal notranslate"><span class="pre">f</span></code> is continuous if and only if <code class="docutils literal notranslate"><span class="pre">(fun</span> <span class="pre">x</span> <span class="pre">&#8614;</span> <span class="pre">x</span> <span class="pre">i)</span> <span class="pre">&#8728;</span> <span class="pre">f</span></code> is continuous for all <code class="docutils literal notranslate"><span class="pre">i</span></code>.
Let us explore that constraint &#8220;on paper&#8221; using notation <span class="math notranslate nohighlight">\(p_i\)</span> for the projection
<code class="docutils literal notranslate"><span class="pre">(fun</span> <span class="pre">(x</span> <span class="pre">:</span> <span class="pre">&#928;</span> <span class="pre">i,</span> <span class="pre">X</span> <span class="pre">i)</span> <span class="pre">&#8614;</span> <span class="pre">x</span> <span class="pre">i)</span></code>:</p>
<div class="math notranslate nohighlight">
\[\begin{split}(&#8704; i, p_i &#8728; f \text{ continuous}) &amp;&#8660; &#8704; i, (p_i &#8728; f)_* T_Z &#8804; T_{X_i} \\
&amp;&#8660; &#8704; i, (p_i)_* f_* T_Z &#8804; T_{X_i}\\
&amp;&#8660; &#8704; i, f_* T_Z &#8804; (p_i)^*T_{X_i}\\
&amp;&#8660;  f_* T_Z &#8804; \inf \left[(p_i)^*T_{X_i}\right]\end{split}\]</div>
<p>So we see that what is the topology we want on <code class="docutils literal notranslate"><span class="pre">&#928;</span> <span class="pre">i,</span> <span class="pre">X</span> <span class="pre">i</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">&#953;</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">)</span> <span class="o">(</span><span class="n">X</span> <span class="o">:</span> <span class="n">&#953;</span> <span class="bp">&#8594;</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">)</span> <span class="o">(</span><span class="n">T_X</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">i</span><span class="o">,</span> <span class="n">TopologicalSpace</span> <span class="o">(</span><span class="n">X</span> <span class="n">i</span><span class="o">))</span> <span class="o">:</span>
    <span class="o">(</span><span class="k">Pi</span><span class="bp">.</span><span class="n">topologicalSpace</span> <span class="o">:</span> <span class="n">TopologicalSpace</span> <span class="o">(</span><span class="bp">&#8704;</span> <span class="n">i</span><span class="o">,</span> <span class="n">X</span> <span class="n">i</span><span class="o">))</span> <span class="bp">=</span>
      <span class="bp">&#10757;</span> <span class="n">i</span><span class="o">,</span> <span class="n">TopologicalSpace.induced</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="n">i</span><span class="o">)</span> <span class="o">(</span><span class="n">T_X</span> <span class="n">i</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">rfl</span>
</pre></div>
</div>
<p>This ends our tour of how Mathlib thinks that topological spaces fix defects of the theory of metric spaces
by being a more functorial theory and having a complete lattice structure for any fixed type.</p>
</section>
<section id="separation-and-countability">
<h3><span class="section-number">9.3.2. </span>Separation and countability<a class="headerlink" href="#separation-and-countability" title="Permalink to this heading">&#61633;</a></h3>
<p>We saw that the category of topological spaces have very nice properties. The price to pay for
this is existence of rather pathological topological spaces.
There are a number of assumptions you can make on a topological space to ensure its behavior
is closer to what metric spaces do. The most important is <code class="docutils literal notranslate"><span class="pre">T2Space</span></code>, also called &#8220;Hausdorff&#8221;,
that will ensure that limits are unique.
A stronger separation property is <code class="docutils literal notranslate"><span class="pre">T3Space</span></code> that ensures in addition the <cite>RegularSpace</cite> property:
each point has a basis of closed neighborhoods.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">T2Space</span> <span class="n">X</span><span class="o">]</span> <span class="o">{</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">a</span><span class="o">))</span>
    <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">b</span><span class="o">))</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">=</span> <span class="n">b</span> <span class="o">:=</span>
  <span class="n">tendsto_nhds_unique</span> <span class="n">ha</span> <span class="n">hb</span>

<span class="kd">example</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">RegularSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span>
    <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">a</span><span class="o">)</span><span class="bp">.</span><span class="n">HasBasis</span> <span class="o">(</span><span class="k">fun</span> <span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span> <span class="bp">&#8614;</span> <span class="n">s</span> <span class="bp">&#8712;</span> <span class="bp">&#120029;</span> <span class="n">a</span> <span class="bp">&#8743;</span> <span class="n">IsClosed</span> <span class="n">s</span><span class="o">)</span> <span class="n">id</span> <span class="o">:=</span>
  <span class="n">closed_nhds_basis</span> <span class="n">a</span>
</pre></div>
</div>
<p>Note that, in every topological space, each point has a basis of open neighborhood, by definition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span>
    <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">HasBasis</span> <span class="o">(</span><span class="k">fun</span> <span class="n">t</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span> <span class="bp">&#8614;</span> <span class="n">t</span> <span class="bp">&#8712;</span> <span class="bp">&#120029;</span> <span class="n">x</span> <span class="bp">&#8743;</span> <span class="n">IsOpen</span> <span class="n">t</span><span class="o">)</span> <span class="n">id</span> <span class="o">:=</span>
  <span class="n">nhds_basis_opens&#39;</span> <span class="n">x</span>
</pre></div>
</div>
<p>Our main goal is now to prove the basic theorem which allows extension by continuity.
From Bourbaki&#8217;s general topology book, I.8.5, Theorem 1 (taking only the non-trivial implication):</p>
<p>Let <span class="math notranslate nohighlight">\(X\)</span> be a topological space, <span class="math notranslate nohighlight">\(A\)</span> a dense subset of <span class="math notranslate nohighlight">\(X\)</span>, <span class="math notranslate nohighlight">\(f : A &#8594; Y\)</span>
a continuous mapping of <span class="math notranslate nohighlight">\(A\)</span> into a <span class="math notranslate nohighlight">\(T_3\)</span> space <span class="math notranslate nohighlight">\(Y\)</span>. If, for each <span class="math notranslate nohighlight">\(x\)</span> in
<span class="math notranslate nohighlight">\(X\)</span>, <span class="math notranslate nohighlight">\(f(y)\)</span> tends to a limit in <span class="math notranslate nohighlight">\(Y\)</span> when <span class="math notranslate nohighlight">\(y\)</span> tends to <span class="math notranslate nohighlight">\(x\)</span>
while remaining in <span class="math notranslate nohighlight">\(A\)</span> then there exists a continuous extension <span class="math notranslate nohighlight">\(&#966;\)</span> of <span class="math notranslate nohighlight">\(f\)</span> to
<span class="math notranslate nohighlight">\(X\)</span>.</p>
<p>Actually Mathlib contains a more general version of the above lemma, <code class="docutils literal notranslate"><span class="pre">DenseInducing.continuousAt_extend</span></code>,
but we&#8217;ll stick to Bourbaki&#8217;s version here.</p>
<p>Remember that, given <code class="docutils literal notranslate"><span class="pre">A</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">X</span></code>, <code class="docutils literal notranslate"><span class="pre">&#8613;A</span></code> is the subtype associated to <code class="docutils literal notranslate"><span class="pre">A</span></code>, and Lean will automatically
insert that funny up arrow when needed. And the (inclusion) coercion map is <code class="docutils literal notranslate"><span class="pre">(&#8593;)</span> <span class="pre">:</span> <span class="pre">A</span> <span class="pre">&#8594;</span> <span class="pre">X</span></code>.
The assumption &#8220;tends to <span class="math notranslate nohighlight">\(x\)</span> while remaining in <span class="math notranslate nohighlight">\(A\)</span>&#8221; corresponds to the pull-back filter
<code class="docutils literal notranslate"><span class="pre">comap</span> <span class="pre">(&#8593;)</span> <span class="pre">(&#120029;</span> <span class="pre">x)</span></code>.</p>
<p>Let&#8217;s prove first an auxiliary lemma, extracted to simplify the context
(in particular we don&#8217;t need Y to be a topological space here).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">aux</span> <span class="o">{</span><span class="n">X</span> <span class="n">Y</span> <span class="n">A</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">{</span><span class="n">c</span> <span class="o">:</span> <span class="n">A</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span>
      <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">A</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">Y</span><span class="o">}</span>
      <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">Tendsto</span> <span class="n">f</span> <span class="o">(</span><span class="n">comap</span> <span class="n">c</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x</span><span class="o">))</span> <span class="n">F</span><span class="o">)</span> <span class="o">{</span><span class="n">V&#39;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">V&#39;_in</span> <span class="o">:</span> <span class="n">V&#39;</span> <span class="bp">&#8712;</span> <span class="n">F</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#8707;</span> <span class="n">V</span> <span class="bp">&#8712;</span> <span class="bp">&#120029;</span> <span class="n">x</span><span class="o">,</span> <span class="n">IsOpen</span> <span class="n">V</span> <span class="bp">&#8743;</span> <span class="n">c</span> <span class="bp">&#8315;&#185;&#39;</span> <span class="n">V</span> <span class="bp">&#8838;</span> <span class="n">f</span> <span class="bp">&#8315;&#185;&#39;</span> <span class="n">V&#39;</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>Let&#8217;s now turn to the main proof of the extension by continuity theorem.</p>
<p>When Lean needs a topology on <code class="docutils literal notranslate"><span class="pre">&#8613;A</span></code> it will automatically use the induced topology.
The only relevant lemma is
<code class="docutils literal notranslate"><span class="pre">nhds_induced</span> <span class="pre">(&#8593;)</span> <span class="pre">:</span> <span class="pre">&#8704;</span> <span class="pre">a</span> <span class="pre">:</span> <span class="pre">&#8613;A,</span> <span class="pre">&#120029;</span> <span class="pre">a</span> <span class="pre">=</span> <span class="pre">comap</span> <span class="pre">(&#8593;)</span> <span class="pre">(&#120029;</span> <span class="pre">&#8593;a)</span></code>
(this is actually a general lemma about induced topologies).</p>
<p>The proof outline is:</p>
<p>The main assumption and the axiom of choice give a function <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> such that
<code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">x,</span> <span class="pre">Tendsto</span> <span class="pre">f</span> <span class="pre">(comap</span> <span class="pre">(&#8593;)</span> <span class="pre">(&#120029;</span> <span class="pre">x))</span> <span class="pre">(&#120029;</span> <span class="pre">(&#966;</span> <span class="pre">x))</span></code>
(because <code class="docutils literal notranslate"><span class="pre">Y</span></code> is Hausdorff, <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> is entirely determined, but we won&#8217;t need that until we try to
prove that <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> indeed extends <code class="docutils literal notranslate"><span class="pre">f</span></code>).</p>
<p>Let&#8217;s first prove <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> is continuous. Fix any <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">:</span> <span class="pre">X</span></code>.
Since <code class="docutils literal notranslate"><span class="pre">Y</span></code> is regular, it suffices to check that for every <em>closed</em> neighborhood
<code class="docutils literal notranslate"><span class="pre">V'</span></code> of <code class="docutils literal notranslate"><span class="pre">&#966;</span> <span class="pre">x</span></code>, <code class="docutils literal notranslate"><span class="pre">&#966;</span> <span class="pre">&#8315;&#185;'</span> <span class="pre">V'</span> <span class="pre">&#8712;</span> <span class="pre">&#120029;</span> <span class="pre">x</span></code>.
The limit assumption gives (through the auxiliary lemma above)
some <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">&#120029;</span> <span class="pre">x</span></code> such <code class="docutils literal notranslate"><span class="pre">IsOpen</span> <span class="pre">V</span> <span class="pre">&#8743;</span> <span class="pre">(&#8593;)</span> <span class="pre">&#8315;&#185;'</span> <span class="pre">V</span> <span class="pre">&#8838;</span> <span class="pre">f</span> <span class="pre">&#8315;&#185;'</span> <span class="pre">V'</span></code>.
Since <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">&#120029;</span> <span class="pre">x</span></code>, it suffices to prove <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8838;</span> <span class="pre">&#966;</span> <span class="pre">&#8315;&#185;'</span> <span class="pre">V'</span></code>, ie  <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">y</span> <span class="pre">&#8712;</span> <span class="pre">V,</span> <span class="pre">&#966;</span> <span class="pre">y</span> <span class="pre">&#8712;</span> <span class="pre">V'</span></code>.
Let&#8217;s fix <code class="docutils literal notranslate"><span class="pre">y</span></code> in <code class="docutils literal notranslate"><span class="pre">V</span></code>. Because <code class="docutils literal notranslate"><span class="pre">V</span></code> is <em>open</em>, it is a neighborhood of <code class="docutils literal notranslate"><span class="pre">y</span></code>.
In particular <code class="docutils literal notranslate"><span class="pre">(&#8593;)</span> <span class="pre">&#8315;&#185;'</span> <span class="pre">V</span> <span class="pre">&#8712;</span> <span class="pre">comap</span> <span class="pre">(&#8593;)</span> <span class="pre">(&#120029;</span> <span class="pre">y)</span></code> and a fortiori <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">&#8315;&#185;'</span> <span class="pre">V'</span> <span class="pre">&#8712;</span> <span class="pre">comap</span> <span class="pre">(&#8593;)</span> <span class="pre">(&#120029;</span> <span class="pre">y)</span></code>.
In addition <code class="docutils literal notranslate"><span class="pre">comap</span> <span class="pre">(&#8593;)</span> <span class="pre">(&#120029;</span> <span class="pre">y)</span> <span class="pre">&#8800;</span> <span class="pre">&#8869;</span></code> because <code class="docutils literal notranslate"><span class="pre">A</span></code> is dense.
Because we know <code class="docutils literal notranslate"><span class="pre">Tendsto</span> <span class="pre">f</span> <span class="pre">(comap</span> <span class="pre">(&#8593;)</span> <span class="pre">(&#120029;</span> <span class="pre">y))</span> <span class="pre">(&#120029;</span> <span class="pre">(&#966;</span> <span class="pre">y))</span></code> this implies
<code class="docutils literal notranslate"><span class="pre">&#966;</span> <span class="pre">y</span> <span class="pre">&#8712;</span> <span class="pre">closure</span> <span class="pre">V'</span></code> and, since <code class="docutils literal notranslate"><span class="pre">V'</span></code> is closed, we have proved <code class="docutils literal notranslate"><span class="pre">&#966;</span> <span class="pre">y</span> <span class="pre">&#8712;</span> <span class="pre">V'</span></code>.</p>
<p>It remains to prove that <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> extends <code class="docutils literal notranslate"><span class="pre">f</span></code>. This is were continuity of <code class="docutils literal notranslate"><span class="pre">f</span></code> enters the discussion,
together with the fact that <code class="docutils literal notranslate"><span class="pre">Y</span></code> is Hausdorff.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">[</span><span class="n">T3Space</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">A</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span>
    <span class="o">(</span><span class="n">hA</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">x</span><span class="o">,</span> <span class="n">x</span> <span class="bp">&#8712;</span> <span class="n">closure</span> <span class="n">A</span><span class="o">)</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">A</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">f_cont</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span>
    <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">c</span> <span class="o">:</span> <span class="n">Y</span><span class="o">,</span> <span class="n">Tendsto</span> <span class="n">f</span> <span class="o">(</span><span class="n">comap</span> <span class="o">(</span><span class="bp">&#8593;</span><span class="o">)</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x</span><span class="o">))</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">c</span><span class="o">))</span> <span class="o">:</span>
    <span class="bp">&#8707;</span> <span class="n">&#966;</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">,</span> <span class="n">Continuous</span> <span class="n">&#966;</span> <span class="bp">&#8743;</span> <span class="bp">&#8704;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">A</span><span class="o">,</span> <span class="n">&#966;</span> <span class="n">a</span> <span class="bp">=</span> <span class="n">f</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="k">#check</span> <span class="n">HasBasis.tendsto_right_iff</span>
</pre></div>
</div>
<p>In addition to separation property, the main kind of assumption you can make on a topological
space to bring it closer to metric spaces is countability assumption. The main one is first countability
asking that every point has a countable neighborhood basic. In particular this ensures that closure
of sets can be understood using sequences.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">]</span> <span class="o">[</span><span class="n">TopologicalSpace.FirstCountableTopology</span> <span class="n">X</span><span class="o">]</span>
      <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">closure</span> <span class="n">s</span> <span class="bp">&#8596;</span> <span class="bp">&#8707;</span> <span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">,</span> <span class="o">(</span><span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">u</span> <span class="n">n</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">)</span> <span class="bp">&#8743;</span> <span class="n">Tendsto</span> <span class="n">u</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">a</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">mem_closure_iff_seq_limit</span>
</pre></div>
</div>
</section>
<section id="id5">
<h3><span class="section-number">9.3.3. </span>Compactness<a class="headerlink" href="#id5" title="Permalink to this heading">&#61633;</a></h3>
<p>Let us now discuss how compactness is defined for topological spaces. As usual there are several ways
to think about it and Mathlib goes for the filter version.</p>
<p>We first need to define cluster points of filters. Given a filter <code class="docutils literal notranslate"><span class="pre">F</span></code> on a topological space <code class="docutils literal notranslate"><span class="pre">X</span></code>,
a point <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">:</span> <span class="pre">X</span></code> is a cluster point of <code class="docutils literal notranslate"><span class="pre">F</span></code> if <code class="docutils literal notranslate"><span class="pre">F</span></code>, seen as a generalized set, has non-empty intersection
with the generalized set of points that are close to <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
<p>Then we can say that a set <code class="docutils literal notranslate"><span class="pre">s</span></code> is compact if every nonempty generalized set <code class="docutils literal notranslate"><span class="pre">F</span></code> contained in <code class="docutils literal notranslate"><span class="pre">s</span></code>,
ie such that <code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">&#8804;</span> <span class="pre">&#120031;</span> <span class="pre">s</span></code>, has a cluster point in <code class="docutils literal notranslate"><span class="pre">s</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">X</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span> <span class="n">ClusterPt</span> <span class="n">x</span> <span class="n">F</span> <span class="bp">&#8596;</span> <span class="n">NeBot</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">x</span> <span class="bp">&#8851;</span> <span class="n">F</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">Iff.rfl</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">:</span>
    <span class="n">IsCompact</span> <span class="n">s</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">X</span><span class="o">)</span> <span class="o">[</span><span class="n">NeBot</span> <span class="n">F</span><span class="o">],</span> <span class="n">F</span> <span class="bp">&#8804;</span> <span class="bp">&#120031;</span> <span class="n">s</span> <span class="bp">&#8594;</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="n">ClusterPt</span> <span class="n">a</span> <span class="n">F</span> <span class="o">:=</span>
  <span class="n">Iff.rfl</span>
</pre></div>
</div>
<p>For instance if <code class="docutils literal notranslate"><span class="pre">F</span></code> is <code class="docutils literal notranslate"><span class="pre">map</span> <span class="pre">u</span> <span class="pre">atTop</span></code>, the image under <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">:</span> <span class="pre">&#8469;</span> <span class="pre">&#8594;</span> <span class="pre">X</span></code> of <code class="docutils literal notranslate"><span class="pre">atTop</span></code>, the generalized set
of very large natural numbers, then the assumption <code class="docutils literal notranslate"><span class="pre">F</span> <span class="pre">&#8804;</span> <span class="pre">&#120031;</span> <span class="pre">s</span></code> means that <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">n</span></code> belongs to <code class="docutils literal notranslate"><span class="pre">s</span></code> for <code class="docutils literal notranslate"><span class="pre">n</span></code>
large enough. Saying that <code class="docutils literal notranslate"><span class="pre">x</span></code> is a cluster point of <code class="docutils literal notranslate"><span class="pre">map</span> <span class="pre">u</span> <span class="pre">atTop</span></code> says the image of very large numbers
intersects the set of points that are close to <code class="docutils literal notranslate"><span class="pre">x</span></code>. In case <code class="docutils literal notranslate"><span class="pre">&#120029;</span> <span class="pre">x</span></code> has a countable basis, we can
interpret this as saying that <code class="docutils literal notranslate"><span class="pre">u</span></code> has a subsequence converging to <code class="docutils literal notranslate"><span class="pre">x</span></code>, and we get back what compactness
looks like in metric spaces.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">TopologicalSpace.FirstCountableTopology</span> <span class="n">X</span><span class="o">]</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">u</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="n">s</span><span class="o">)</span>
    <span class="o">(</span><span class="n">hu</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">n</span><span class="o">,</span> <span class="n">u</span> <span class="n">n</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="bp">&#8712;</span> <span class="n">s</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">&#966;</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="n">StrictMono</span> <span class="n">&#966;</span> <span class="bp">&#8743;</span> <span class="n">Tendsto</span> <span class="o">(</span><span class="n">u</span> <span class="bp">&#8728;</span> <span class="n">&#966;</span><span class="o">)</span> <span class="n">atTop</span> <span class="o">(</span><span class="bp">&#120029;</span> <span class="n">a</span><span class="o">)</span> <span class="o">:=</span>
  <span class="n">hs.tendsto_subseq</span> <span class="n">hu</span>
</pre></div>
</div>
<p>Cluster points behave nicely with continuous functions.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">Y</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">F</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">X</span><span class="o">}</span> <span class="o">{</span><span class="n">G</span> <span class="o">:</span> <span class="n">Filter</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">H</span> <span class="o">:</span> <span class="n">ClusterPt</span> <span class="n">x</span> <span class="n">F</span><span class="o">)</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span>
    <span class="o">(</span><span class="n">hfx</span> <span class="o">:</span> <span class="n">ContinuousAt</span> <span class="n">f</span> <span class="n">x</span><span class="o">)</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Tendsto</span> <span class="n">f</span> <span class="n">F</span> <span class="n">G</span><span class="o">)</span> <span class="o">:</span> <span class="n">ClusterPt</span> <span class="o">(</span><span class="n">f</span> <span class="n">x</span><span class="o">)</span> <span class="n">G</span> <span class="o">:=</span>
  <span class="n">ClusterPt.map</span> <span class="n">H</span> <span class="n">hfx</span> <span class="n">hf</span>
</pre></div>
</div>
<p>As an exercise, we will prove that the image of a compact set under a continuous map is
compact. In addition to what we saw already, you should use <code class="docutils literal notranslate"><span class="pre">Filter.push_pull</span></code> and
<code class="docutils literal notranslate"><span class="pre">NeBot.of_map</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">[</span><span class="n">TopologicalSpace</span> <span class="n">Y</span><span class="o">]</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Continuous</span> <span class="n">f</span><span class="o">)</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">IsCompact</span> <span class="o">(</span><span class="n">f</span> <span class="bp">&#39;&#39;</span> <span class="n">s</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">F</span> <span class="n">F_ne</span> <span class="n">F_le</span>
  <span class="k">have</span> <span class="n">map_eq</span> <span class="o">:</span> <span class="n">map</span> <span class="n">f</span> <span class="o">(</span><span class="bp">&#120031;</span> <span class="n">s</span> <span class="bp">&#8851;</span> <span class="n">comap</span> <span class="n">f</span> <span class="n">F</span><span class="o">)</span> <span class="bp">=</span> <span class="bp">&#120031;</span> <span class="o">(</span><span class="n">f</span> <span class="bp">&#39;&#39;</span> <span class="n">s</span><span class="o">)</span> <span class="bp">&#8851;</span> <span class="n">F</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="k">have</span> <span class="n">Hne</span> <span class="o">:</span> <span class="o">(</span><span class="bp">&#120031;</span> <span class="n">s</span> <span class="bp">&#8851;</span> <span class="n">comap</span> <span class="n">f</span> <span class="n">F</span><span class="o">)</span><span class="bp">.</span><span class="n">NeBot</span> <span class="o">:=</span> <span class="kd">by</span> <span class="gr">sorry</span>
  <span class="k">have</span> <span class="n">Hle</span> <span class="o">:</span> <span class="bp">&#120031;</span> <span class="n">s</span> <span class="bp">&#8851;</span> <span class="n">comap</span> <span class="n">f</span> <span class="n">F</span> <span class="bp">&#8804;</span> <span class="bp">&#120031;</span> <span class="n">s</span> <span class="o">:=</span> <span class="n">inf_le_left</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>One can also express compactness in terms of open covers: <code class="docutils literal notranslate"><span class="pre">s</span></code> is compact if every family of open sets that
cover <code class="docutils literal notranslate"><span class="pre">s</span></code> has a finite covering sub-family.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">&#953;</span> <span class="o">:</span> <span class="kt">Type</span><span class="bp">*</span><span class="o">}</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">IsCompact</span> <span class="n">s</span><span class="o">)</span> <span class="o">(</span><span class="n">U</span> <span class="o">:</span> <span class="n">&#953;</span> <span class="bp">&#8594;</span> <span class="n">Set</span> <span class="n">X</span><span class="o">)</span> <span class="o">(</span><span class="n">hUo</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">i</span><span class="o">,</span> <span class="n">IsOpen</span> <span class="o">(</span><span class="n">U</span> <span class="n">i</span><span class="o">))</span>
    <span class="o">(</span><span class="n">hsU</span> <span class="o">:</span> <span class="n">s</span> <span class="bp">&#8838;</span> <span class="bp">&#8899;</span> <span class="n">i</span><span class="o">,</span> <span class="n">U</span> <span class="n">i</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">t</span> <span class="o">:</span> <span class="n">Finset</span> <span class="n">&#953;</span><span class="o">,</span> <span class="n">s</span> <span class="bp">&#8838;</span> <span class="bp">&#8899;</span> <span class="n">i</span> <span class="bp">&#8712;</span> <span class="n">t</span><span class="o">,</span> <span class="n">U</span> <span class="n">i</span> <span class="o">:=</span>
  <span class="n">hs.elim_finite_subcover</span> <span class="n">U</span> <span class="n">hUo</span> <span class="n">hsU</span>
</pre></div>
</div>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C08_Groups_and_Rings.html" class="btn btn-neutral float-left" title="8. Groups and Rings" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C10_Differential_Calculus.html" class="btn btn-neutral float-right" title="10. Differential Calculus" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>