/
Basic.lean
1992 lines (1633 loc) · 97.5 KB
/
Basic.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
-/
import Mathlib.Order.Filter.SmallSets
import Mathlib.Tactic.Monotonicity
import Mathlib.Topology.Compactness.Compact
import Mathlib.Topology.NhdsSet
import Mathlib.Algebra.Group.Defs
#align_import topology.uniform_space.basic from "leanprover-community/mathlib"@"195fcd60ff2bfe392543bceb0ec2adcdb472db4c"
/-!
# Uniform spaces
Uniform spaces are a generalization of metric spaces and topological groups. Many concepts directly
generalize to uniform spaces, e.g.
* uniform continuity (in this file)
* completeness (in `Cauchy.lean`)
* extension of uniform continuous functions to complete spaces (in `UniformEmbedding.lean`)
* totally bounded sets (in `Cauchy.lean`)
* totally bounded complete sets are compact (in `Cauchy.lean`)
A uniform structure on a type `X` is a filter `𝓤 X` on `X × X` satisfying some conditions
which makes it reasonable to say that `∀ᶠ (p : X × X) in 𝓤 X, ...` means
"for all p.1 and p.2 in X close enough, ...". Elements of this filter are called entourages
of `X`. The two main examples are:
* If `X` is a metric space, `V ∈ 𝓤 X ↔ ∃ ε > 0, { p | dist p.1 p.2 < ε } ⊆ V`
* If `G` is an additive topological group, `V ∈ 𝓤 G ↔ ∃ U ∈ 𝓝 (0 : G), {p | p.2 - p.1 ∈ U} ⊆ V`
Those examples are generalizations in two different directions of the elementary example where
`X = ℝ` and `V ∈ 𝓤 ℝ ↔ ∃ ε > 0, { p | |p.2 - p.1| < ε } ⊆ V` which features both the topological
group structure on `ℝ` and its metric space structure.
Each uniform structure on `X` induces a topology on `X` characterized by
> `nhds_eq_comap_uniformity : ∀ {x : X}, 𝓝 x = comap (Prod.mk x) (𝓤 X)`
where `Prod.mk x : X → X × X := (fun y ↦ (x, y))` is the partial evaluation of the product
constructor.
The dictionary with metric spaces includes:
* an upper bound for `dist x y` translates into `(x, y) ∈ V` for some `V ∈ 𝓤 X`
* a ball `ball x r` roughly corresponds to `UniformSpace.ball x V := {y | (x, y) ∈ V}`
for some `V ∈ 𝓤 X`, but the later is more general (it includes in
particular both open and closed balls for suitable `V`).
In particular we have:
`isOpen_iff_ball_subset {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 X, ball x V ⊆ s`
The triangle inequality is abstracted to a statement involving the composition of relations in `X`.
First note that the triangle inequality in a metric space is equivalent to
`∀ (x y z : X) (r r' : ℝ), dist x y ≤ r → dist y z ≤ r' → dist x z ≤ r + r'`.
Then, for any `V` and `W` with type `Set (X × X)`, the composition `V ○ W : Set (X × X)` is
defined as `{ p : X × X | ∃ z, (p.1, z) ∈ V ∧ (z, p.2) ∈ W }`.
In the metric space case, if `V = { p | dist p.1 p.2 ≤ r }` and `W = { p | dist p.1 p.2 ≤ r' }`
then the triangle inequality, as reformulated above, says `V ○ W` is contained in
`{p | dist p.1 p.2 ≤ r + r'}` which is the entourage associated to the radius `r + r'`.
In general we have `mem_ball_comp (h : y ∈ ball x V) (h' : z ∈ ball y W) : z ∈ ball x (V ○ W)`.
Note that this discussion does not depend on any axiom imposed on the uniformity filter,
it is simply captured by the definition of composition.
The uniform space axioms ask the filter `𝓤 X` to satisfy the following:
* every `V ∈ 𝓤 X` contains the diagonal `idRel = { p | p.1 = p.2 }`. This abstracts the fact
that `dist x x ≤ r` for every non-negative radius `r` in the metric space case and also that
`x - x` belongs to every neighborhood of zero in the topological group case.
* `V ∈ 𝓤 X → Prod.swap '' V ∈ 𝓤 X`. This is tightly related the fact that `dist x y = dist y x`
in a metric space, and to continuity of negation in the topological group case.
* `∀ V ∈ 𝓤 X, ∃ W ∈ 𝓤 X, W ○ W ⊆ V`. In the metric space case, it corresponds
to cutting the radius of a ball in half and applying the triangle inequality.
In the topological group case, it comes from continuity of addition at `(0, 0)`.
These three axioms are stated more abstractly in the definition below, in terms of
operations on filters, without directly manipulating entourages.
## Main definitions
* `UniformSpace X` is a uniform space structure on a type `X`
* `UniformContinuous f` is a predicate saying a function `f : α → β` between uniform spaces
is uniformly continuous : `∀ r ∈ 𝓤 β, ∀ᶠ (x : α × α) in 𝓤 α, (f x.1, f x.2) ∈ r`
In this file we also define a complete lattice structure on the type `UniformSpace X`
of uniform structures on `X`, as well as the pullback (`UniformSpace.comap`) of uniform structures
coming from the pullback of filters.
Like distance functions, uniform structures cannot be pushed forward in general.
## Notations
Localized in `Uniformity`, we have the notation `𝓤 X` for the uniformity on a uniform space `X`,
and `○` for composition of relations, seen as terms with type `Set (X × X)`.
## Implementation notes
There is already a theory of relations in `Data/Rel.lean` where the main definition is
`def Rel (α β : Type*) := α → β → Prop`.
The relations used in the current file involve only one type, but this is not the reason why
we don't reuse `Data/Rel.lean`. We use `Set (α × α)`
instead of `Rel α α` because we really need sets to use the filter library, and elements
of filters on `α × α` have type `Set (α × α)`.
The structure `UniformSpace X` bundles a uniform structure on `X`, a topology on `X` and
an assumption saying those are compatible. This may not seem mathematically reasonable at first,
but is in fact an instance of the forgetful inheritance pattern. See Note [forgetful inheritance]
below.
## References
The formalization uses the books:
* [N. Bourbaki, *General Topology*][bourbaki1966]
* [I. M. James, *Topologies and Uniformities*][james1999]
But it makes a more systematic use of the filter library.
-/
open Set Filter Topology
universe u v ua ub uc ud
/-!
### Relations, seen as `Set (α × α)`
-/
variable {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} {ι : Sort*}
/-- The identity relation, or the graph of the identity function -/
def idRel {α : Type*} :=
{ p : α × α | p.1 = p.2 }
#align id_rel idRel
@[simp]
theorem mem_idRel {a b : α} : (a, b) ∈ @idRel α ↔ a = b :=
Iff.rfl
#align mem_id_rel mem_idRel
@[simp]
theorem idRel_subset {s : Set (α × α)} : idRel ⊆ s ↔ ∀ a, (a, a) ∈ s := by
simp [subset_def]
#align id_rel_subset idRel_subset
/-- The composition of relations -/
def compRel (r₁ r₂ : Set (α × α)) :=
{ p : α × α | ∃ z : α, (p.1, z) ∈ r₁ ∧ (z, p.2) ∈ r₂ }
#align comp_rel compRel
@[inherit_doc]
scoped[Uniformity] infixl:62 " ○ " => compRel
open Uniformity
@[simp]
theorem mem_compRel {α : Type u} {r₁ r₂ : Set (α × α)} {x y : α} :
(x, y) ∈ r₁ ○ r₂ ↔ ∃ z, (x, z) ∈ r₁ ∧ (z, y) ∈ r₂ :=
Iff.rfl
#align mem_comp_rel mem_compRel
@[simp]
theorem swap_idRel : Prod.swap '' idRel = @idRel α :=
Set.ext fun ⟨a, b⟩ => by simpa [image_swap_eq_preimage_swap] using eq_comm
#align swap_id_rel swap_idRel
theorem Monotone.compRel [Preorder β] {f g : β → Set (α × α)} (hf : Monotone f) (hg : Monotone g) :
Monotone fun x => f x ○ g x := fun _ _ h _ ⟨z, h₁, h₂⟩ => ⟨z, hf h h₁, hg h h₂⟩
#align monotone.comp_rel Monotone.compRel
@[mono]
theorem compRel_mono {f g h k : Set (α × α)} (h₁ : f ⊆ h) (h₂ : g ⊆ k) : f ○ g ⊆ h ○ k :=
fun _ ⟨z, h, h'⟩ => ⟨z, h₁ h, h₂ h'⟩
#align comp_rel_mono compRel_mono
theorem prod_mk_mem_compRel {a b c : α} {s t : Set (α × α)} (h₁ : (a, c) ∈ s) (h₂ : (c, b) ∈ t) :
(a, b) ∈ s ○ t :=
⟨c, h₁, h₂⟩
#align prod_mk_mem_comp_rel prod_mk_mem_compRel
@[simp]
theorem id_compRel {r : Set (α × α)} : idRel ○ r = r :=
Set.ext fun ⟨a, b⟩ => by simp
#align id_comp_rel id_compRel
theorem compRel_assoc {r s t : Set (α × α)} : r ○ s ○ t = r ○ (s ○ t) := by
ext ⟨a, b⟩; simp only [mem_compRel]; tauto
#align comp_rel_assoc compRel_assoc
theorem left_subset_compRel {s t : Set (α × α)} (h : idRel ⊆ t) : s ⊆ s ○ t := fun ⟨_x, y⟩ xy_in =>
⟨y, xy_in, h <| rfl⟩
#align left_subset_comp_rel left_subset_compRel
theorem right_subset_compRel {s t : Set (α × α)} (h : idRel ⊆ s) : t ⊆ s ○ t := fun ⟨x, _y⟩ xy_in =>
⟨x, h <| rfl, xy_in⟩
#align right_subset_comp_rel right_subset_compRel
theorem subset_comp_self {s : Set (α × α)} (h : idRel ⊆ s) : s ⊆ s ○ s :=
left_subset_compRel h
#align subset_comp_self subset_comp_self
theorem subset_iterate_compRel {s t : Set (α × α)} (h : idRel ⊆ s) (n : ℕ) :
t ⊆ (s ○ ·)^[n] t := by
induction' n with n ihn generalizing t
exacts [Subset.rfl, (right_subset_compRel h).trans ihn]
#align subset_iterate_comp_rel subset_iterate_compRel
/-- The relation is invariant under swapping factors. -/
def SymmetricRel (V : Set (α × α)) : Prop :=
Prod.swap ⁻¹' V = V
#align symmetric_rel SymmetricRel
/-- The maximal symmetric relation contained in a given relation. -/
def symmetrizeRel (V : Set (α × α)) : Set (α × α) :=
V ∩ Prod.swap ⁻¹' V
#align symmetrize_rel symmetrizeRel
theorem symmetric_symmetrizeRel (V : Set (α × α)) : SymmetricRel (symmetrizeRel V) := by
simp [SymmetricRel, symmetrizeRel, preimage_inter, inter_comm, ← preimage_comp]
#align symmetric_symmetrize_rel symmetric_symmetrizeRel
theorem symmetrizeRel_subset_self (V : Set (α × α)) : symmetrizeRel V ⊆ V :=
sep_subset _ _
#align symmetrize_rel_subset_self symmetrizeRel_subset_self
@[mono]
theorem symmetrize_mono {V W : Set (α × α)} (h : V ⊆ W) : symmetrizeRel V ⊆ symmetrizeRel W :=
inter_subset_inter h <| preimage_mono h
#align symmetrize_mono symmetrize_mono
theorem SymmetricRel.mk_mem_comm {V : Set (α × α)} (hV : SymmetricRel V) {x y : α} :
(x, y) ∈ V ↔ (y, x) ∈ V :=
Set.ext_iff.1 hV (y, x)
#align symmetric_rel.mk_mem_comm SymmetricRel.mk_mem_comm
theorem SymmetricRel.eq {U : Set (α × α)} (hU : SymmetricRel U) : Prod.swap ⁻¹' U = U :=
hU
#align symmetric_rel.eq SymmetricRel.eq
theorem SymmetricRel.inter {U V : Set (α × α)} (hU : SymmetricRel U) (hV : SymmetricRel V) :
SymmetricRel (U ∩ V) := by rw [SymmetricRel, preimage_inter, hU.eq, hV.eq]
#align symmetric_rel.inter SymmetricRel.inter
/-- This core description of a uniform space is outside of the type class hierarchy. It is useful
for constructions of uniform spaces, when the topology is derived from the uniform space. -/
structure UniformSpace.Core (α : Type u) where
/-- The uniformity filter. Once `UniformSpace` is defined, `𝓤 α` (`_root_.uniformity`) becomes the
normal form. -/
uniformity : Filter (α × α)
/-- Every set in the uniformity filter includes the diagonal. -/
refl : 𝓟 idRel ≤ uniformity
/-- If `s ∈ uniformity`, then `Prod.swap ⁻¹' s ∈ uniformity`. -/
symm : Tendsto Prod.swap uniformity uniformity
/-- For every set `u ∈ uniformity`, there exists `v ∈ uniformity` such that `v ○ v ⊆ u`. -/
comp : (uniformity.lift' fun s => s ○ s) ≤ uniformity
#align uniform_space.core UniformSpace.Core
protected theorem UniformSpace.Core.comp_mem_uniformity_sets {c : Core α} {s : Set (α × α)}
(hs : s ∈ c.uniformity) : ∃ t ∈ c.uniformity, t ○ t ⊆ s :=
(mem_lift'_sets <| monotone_id.compRel monotone_id).mp <| c.comp hs
/-- An alternative constructor for `UniformSpace.Core`. This version unfolds various
`Filter`-related definitions. -/
def UniformSpace.Core.mk' {α : Type u} (U : Filter (α × α)) (refl : ∀ r ∈ U, ∀ (x), (x, x) ∈ r)
(symm : ∀ r ∈ U, Prod.swap ⁻¹' r ∈ U) (comp : ∀ r ∈ U, ∃ t ∈ U, t ○ t ⊆ r) :
UniformSpace.Core α :=
⟨U, fun _r ru => idRel_subset.2 (refl _ ru), symm, fun _r ru =>
let ⟨_s, hs, hsr⟩ := comp _ ru
mem_of_superset (mem_lift' hs) hsr⟩
#align uniform_space.core.mk' UniformSpace.Core.mk'
/-- Defining a `UniformSpace.Core` from a filter basis satisfying some uniformity-like axioms. -/
def UniformSpace.Core.mkOfBasis {α : Type u} (B : FilterBasis (α × α))
(refl : ∀ r ∈ B, ∀ (x), (x, x) ∈ r) (symm : ∀ r ∈ B, ∃ t ∈ B, t ⊆ Prod.swap ⁻¹' r)
(comp : ∀ r ∈ B, ∃ t ∈ B, t ○ t ⊆ r) : UniformSpace.Core α where
uniformity := B.filter
refl := B.hasBasis.ge_iff.mpr fun _r ru => idRel_subset.2 <| refl _ ru
symm := (B.hasBasis.tendsto_iff B.hasBasis).mpr symm
comp := (HasBasis.le_basis_iff (B.hasBasis.lift' (monotone_id.compRel monotone_id))
B.hasBasis).2 comp
#align uniform_space.core.mk_of_basis UniformSpace.Core.mkOfBasis
/-- A uniform space generates a topological space -/
def UniformSpace.Core.toTopologicalSpace {α : Type u} (u : UniformSpace.Core α) :
TopologicalSpace α :=
.mkOfNhds fun x ↦ .comap (Prod.mk x) u.uniformity
#align uniform_space.core.to_topological_space UniformSpace.Core.toTopologicalSpace
theorem UniformSpace.Core.ext :
∀ {u₁ u₂ : UniformSpace.Core α}, u₁.uniformity = u₂.uniformity → u₁ = u₂
| ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl
#align uniform_space.core_eq UniformSpace.Core.ext
theorem UniformSpace.Core.nhds_toTopologicalSpace {α : Type u} (u : Core α) (x : α) :
@nhds α u.toTopologicalSpace x = comap (Prod.mk x) u.uniformity := by
apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun _ ↦ (basis_sets _).comap _)
· exact fun a U hU ↦ u.refl hU rfl
· intro a U hU
rcases u.comp_mem_uniformity_sets hU with ⟨V, hV, hVU⟩
filter_upwards [preimage_mem_comap hV] with b hb
filter_upwards [preimage_mem_comap hV] with c hc
exact hVU ⟨b, hb, hc⟩
-- the topological structure is embedded in the uniform structure
-- to avoid instance diamond issues. See Note [forgetful inheritance].
/-- A uniform space is a generalization of the "uniform" topological aspects of a
metric space. It consists of a filter on `α × α` called the "uniformity", which
satisfies properties analogous to the reflexivity, symmetry, and triangle properties
of a metric.
A metric space has a natural uniformity, and a uniform space has a natural topology.
A topological group also has a natural uniformity, even when it is not metrizable. -/
class UniformSpace (α : Type u) extends TopologicalSpace α where
/-- The uniformity filter. -/
protected uniformity : Filter (α × α)
/-- If `s ∈ uniformity`, then `Prod.swap ⁻¹' s ∈ uniformity`. -/
protected symm : Tendsto Prod.swap uniformity uniformity
/-- For every set `u ∈ uniformity`, there exists `v ∈ uniformity` such that `v ○ v ⊆ u`. -/
protected comp : (uniformity.lift' fun s => s ○ s) ≤ uniformity
/-- The uniformity agrees with the topology: the neighborhoods filter of each point `x`
is equal to `Filter.comap (Prod.mk x) (𝓤 α)`. -/
protected nhds_eq_comap_uniformity (x : α) : 𝓝 x = comap (Prod.mk x) uniformity
#align uniform_space UniformSpace
#noalign uniform_space.mk' -- Can't be a `match_pattern`, so not useful anymore
/-- The uniformity is a filter on α × α (inferred from an ambient uniform space
structure on α). -/
def uniformity (α : Type u) [UniformSpace α] : Filter (α × α) :=
@UniformSpace.uniformity α _
#align uniformity uniformity
/-- Notation for the uniformity filter with respect to a non-standard `UniformSpace` instance. -/
scoped[Uniformity] notation "𝓤[" u "]" => @uniformity _ u
@[inherit_doc] -- Porting note (#11215): TODO: should we drop the `uniformity` def?
scoped[Uniformity] notation "𝓤" => uniformity
/-- Construct a `UniformSpace` from a `u : UniformSpace.Core` and a `TopologicalSpace` structure
that is equal to `u.toTopologicalSpace`. -/
abbrev UniformSpace.ofCoreEq {α : Type u} (u : UniformSpace.Core α) (t : TopologicalSpace α)
(h : t = u.toTopologicalSpace) : UniformSpace α where
__ := u
toTopologicalSpace := t
nhds_eq_comap_uniformity x := by rw [h, u.nhds_toTopologicalSpace]
#align uniform_space.of_core_eq UniformSpace.ofCoreEq
/-- Construct a `UniformSpace` from a `UniformSpace.Core`. -/
abbrev UniformSpace.ofCore {α : Type u} (u : UniformSpace.Core α) : UniformSpace α :=
.ofCoreEq u _ rfl
#align uniform_space.of_core UniformSpace.ofCore
/-- Construct a `UniformSpace.Core` from a `UniformSpace`. -/
abbrev UniformSpace.toCore (u : UniformSpace α) : UniformSpace.Core α where
__ := u
refl := by
rintro U hU ⟨x, y⟩ (rfl : x = y)
have : Prod.mk x ⁻¹' U ∈ 𝓝 x := by
rw [UniformSpace.nhds_eq_comap_uniformity]
exact preimage_mem_comap hU
convert mem_of_mem_nhds this
theorem UniformSpace.toCore_toTopologicalSpace (u : UniformSpace α) :
u.toCore.toTopologicalSpace = u.toTopologicalSpace :=
TopologicalSpace.ext_nhds fun a ↦ by
rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]
#align uniform_space.to_core_to_topological_space UniformSpace.toCore_toTopologicalSpace
/-- Build a `UniformSpace` from a `UniformSpace.Core` and a compatible topology.
Use `UnifiormSpace.mk` instead to avoid proving
the unnecessary assumption `UniformSpace.Core.refl`.
The main constructor used to use a different compatibility assumption.
This definition was created as a step towards porting to a new definition.
Now the main definition is ported,
so this constructor will be removed in a few months. -/
@[deprecated UniformSpace.mk]
def UniformSpace.ofNhdsEqComap (u : UniformSpace.Core α) (_t : TopologicalSpace α)
(h : ∀ x, 𝓝 x = u.uniformity.comap (Prod.mk x)) : UniformSpace α where
__ := u
nhds_eq_comap_uniformity := h
@[ext]
protected theorem UniformSpace.ext {u₁ u₂ : UniformSpace α} (h : 𝓤[u₁] = 𝓤[u₂]) : u₁ = u₂ := by
have : u₁.toTopologicalSpace = u₂.toTopologicalSpace := TopologicalSpace.ext_nhds fun x ↦ by
rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
exact congr_arg (comap _) h
cases u₁; cases u₂; congr
#align uniform_space_eq UniformSpace.ext
protected theorem UniformSpace.ext_iff {u₁ u₂ : UniformSpace α} :
u₁ = u₂ ↔ ∀ s, s ∈ 𝓤[u₁] ↔ s ∈ 𝓤[u₂] :=
⟨fun h _ => h ▸ Iff.rfl, fun h => by ext; exact h _⟩
theorem UniformSpace.ofCoreEq_toCore (u : UniformSpace α) (t : TopologicalSpace α)
(h : t = u.toCore.toTopologicalSpace) : .ofCoreEq u.toCore t h = u :=
UniformSpace.ext rfl
#align uniform_space.of_core_eq_to_core UniformSpace.ofCoreEq_toCore
/-- Replace topology in a `UniformSpace` instance with a propositionally (but possibly not
definitionally) equal one. -/
abbrev UniformSpace.replaceTopology {α : Type*} [i : TopologicalSpace α] (u : UniformSpace α)
(h : i = u.toTopologicalSpace) : UniformSpace α where
__ := u
toTopologicalSpace := i
nhds_eq_comap_uniformity x := by rw [h, u.nhds_eq_comap_uniformity]
#align uniform_space.replace_topology UniformSpace.replaceTopology
theorem UniformSpace.replaceTopology_eq {α : Type*} [i : TopologicalSpace α] (u : UniformSpace α)
(h : i = u.toTopologicalSpace) : u.replaceTopology h = u :=
UniformSpace.ext rfl
#align uniform_space.replace_topology_eq UniformSpace.replaceTopology_eq
-- Porting note: rfc: use `UniformSpace.Core.mkOfBasis`? This will change defeq here and there
/-- Define a `UniformSpace` using a "distance" function. The function can be, e.g., the
distance in a (usual or extended) metric space or an absolute value on a ring. -/
def UniformSpace.ofFun {α : Type u} {β : Type v} [OrderedAddCommMonoid β]
(d : α → α → β) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)
(half : ∀ ε > (0 : β), ∃ δ > (0 : β), ∀ x < δ, ∀ y < δ, x + y < ε) :
UniformSpace α :=
.ofCore
{ uniformity := ⨅ r > 0, 𝓟 { x | d x.1 x.2 < r }
refl := le_iInf₂ fun r hr => principal_mono.2 <| idRel_subset.2 fun x => by simpa [refl]
symm := tendsto_iInf_iInf fun r => tendsto_iInf_iInf fun _ => tendsto_principal_principal.2
fun x hx => by rwa [mem_setOf, symm]
comp := le_iInf₂ fun r hr => let ⟨δ, h0, hδr⟩ := half r hr; le_principal_iff.2 <|
mem_of_superset
(mem_lift' <| mem_iInf_of_mem δ <| mem_iInf_of_mem h0 <| mem_principal_self _)
fun (x, z) ⟨y, h₁, h₂⟩ => (triangle _ _ _).trans_lt (hδr _ h₁ _ h₂) }
#align uniform_space.of_fun UniformSpace.ofFun
theorem UniformSpace.hasBasis_ofFun {α : Type u} {β : Type v} [LinearOrderedAddCommMonoid β]
(h₀ : ∃ x : β, 0 < x) (d : α → α → β) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)
(half : ∀ ε > (0 : β), ∃ δ > (0 : β), ∀ x < δ, ∀ y < δ, x + y < ε) :
𝓤[.ofFun d refl symm triangle half].HasBasis ((0 : β) < ·) (fun ε => { x | d x.1 x.2 < ε }) :=
hasBasis_biInf_principal'
(fun ε₁ h₁ ε₂ h₂ => ⟨min ε₁ ε₂, lt_min h₁ h₂, fun _x hx => lt_of_lt_of_le hx (min_le_left _ _),
fun _x hx => lt_of_lt_of_le hx (min_le_right _ _)⟩) h₀
#align uniform_space.has_basis_of_fun UniformSpace.hasBasis_ofFun
section UniformSpace
variable [UniformSpace α]
theorem nhds_eq_comap_uniformity {x : α} : 𝓝 x = (𝓤 α).comap (Prod.mk x) :=
UniformSpace.nhds_eq_comap_uniformity x
#align nhds_eq_comap_uniformity nhds_eq_comap_uniformity
theorem isOpen_uniformity {s : Set α} :
IsOpen s ↔ ∀ x ∈ s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ 𝓤 α := by
simp only [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap_prod_mk]
#align is_open_uniformity isOpen_uniformity
theorem refl_le_uniformity : 𝓟 idRel ≤ 𝓤 α :=
(@UniformSpace.toCore α _).refl
#align refl_le_uniformity refl_le_uniformity
instance uniformity.neBot [Nonempty α] : NeBot (𝓤 α) :=
diagonal_nonempty.principal_neBot.mono refl_le_uniformity
#align uniformity.ne_bot uniformity.neBot
theorem refl_mem_uniformity {x : α} {s : Set (α × α)} (h : s ∈ 𝓤 α) : (x, x) ∈ s :=
refl_le_uniformity h rfl
#align refl_mem_uniformity refl_mem_uniformity
theorem mem_uniformity_of_eq {x y : α} {s : Set (α × α)} (h : s ∈ 𝓤 α) (hx : x = y) : (x, y) ∈ s :=
refl_le_uniformity h hx
#align mem_uniformity_of_eq mem_uniformity_of_eq
theorem symm_le_uniformity : map (@Prod.swap α α) (𝓤 _) ≤ 𝓤 _ :=
UniformSpace.symm
#align symm_le_uniformity symm_le_uniformity
theorem comp_le_uniformity : ((𝓤 α).lift' fun s : Set (α × α) => s ○ s) ≤ 𝓤 α :=
UniformSpace.comp
#align comp_le_uniformity comp_le_uniformity
theorem lift'_comp_uniformity : ((𝓤 α).lift' fun s : Set (α × α) => s ○ s) = 𝓤 α :=
comp_le_uniformity.antisymm <| le_lift'.2 fun _s hs ↦ mem_of_superset hs <|
subset_comp_self <| idRel_subset.2 fun _ ↦ refl_mem_uniformity hs
theorem tendsto_swap_uniformity : Tendsto (@Prod.swap α α) (𝓤 α) (𝓤 α) :=
symm_le_uniformity
#align tendsto_swap_uniformity tendsto_swap_uniformity
theorem comp_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ t ⊆ s :=
(mem_lift'_sets <| monotone_id.compRel monotone_id).mp <| comp_le_uniformity hs
#align comp_mem_uniformity_sets comp_mem_uniformity_sets
/-- If `s ∈ 𝓤 α`, then for any natural `n`, for a subset `t` of a sufficiently small set in `𝓤 α`,
we have `t ○ t ○ ... ○ t ⊆ s` (`n` compositions). -/
theorem eventually_uniformity_iterate_comp_subset {s : Set (α × α)} (hs : s ∈ 𝓤 α) (n : ℕ) :
∀ᶠ t in (𝓤 α).smallSets, (t ○ ·)^[n] t ⊆ s := by
suffices ∀ᶠ t in (𝓤 α).smallSets, t ⊆ s ∧ (t ○ ·)^[n] t ⊆ s from (eventually_and.1 this).2
induction' n with n ihn generalizing s
· simpa
rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
refine' (ihn htU).mono fun U hU => _
rw [Function.iterate_succ_apply']
exact
⟨hU.1.trans <| (subset_comp_self <| refl_le_uniformity htU).trans hts,
(compRel_mono hU.1 hU.2).trans hts⟩
#align eventually_uniformity_iterate_comp_subset eventually_uniformity_iterate_comp_subset
/-- If `s ∈ 𝓤 α`, then for a subset `t` of a sufficiently small set in `𝓤 α`,
we have `t ○ t ⊆ s`. -/
theorem eventually_uniformity_comp_subset {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
∀ᶠ t in (𝓤 α).smallSets, t ○ t ⊆ s :=
eventually_uniformity_iterate_comp_subset hs 1
#align eventually_uniformity_comp_subset eventually_uniformity_comp_subset
/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is transitive. -/
theorem Filter.Tendsto.uniformity_trans {l : Filter β} {f₁ f₂ f₃ : β → α}
(h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α))
(h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)) : Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α) := by
refine' le_trans (le_lift'.2 fun s hs => mem_map.2 _) comp_le_uniformity
filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩
#align filter.tendsto.uniformity_trans Filter.Tendsto.uniformity_trans
/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is symmetric. -/
theorem Filter.Tendsto.uniformity_symm {l : Filter β} {f : β → α × α} (h : Tendsto f l (𝓤 α)) :
Tendsto (fun x => ((f x).2, (f x).1)) l (𝓤 α) :=
tendsto_swap_uniformity.comp h
#align filter.tendsto.uniformity_symm Filter.Tendsto.uniformity_symm
/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is reflexive. -/
theorem tendsto_diag_uniformity (f : β → α) (l : Filter β) :
Tendsto (fun x => (f x, f x)) l (𝓤 α) := fun _s hs =>
mem_map.2 <| univ_mem' fun _ => refl_mem_uniformity hs
#align tendsto_diag_uniformity tendsto_diag_uniformity
theorem tendsto_const_uniformity {a : α} {f : Filter β} : Tendsto (fun _ => (a, a)) f (𝓤 α) :=
tendsto_diag_uniformity (fun _ => a) f
#align tendsto_const_uniformity tendsto_const_uniformity
theorem symm_of_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
∃ t ∈ 𝓤 α, (∀ a b, (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s :=
have : preimage Prod.swap s ∈ 𝓤 α := symm_le_uniformity hs
⟨s ∩ preimage Prod.swap s, inter_mem hs this, fun _ _ ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩, inter_subset_left _ _⟩
#align symm_of_uniformity symm_of_uniformity
theorem comp_symm_of_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
∃ t ∈ 𝓤 α, (∀ {a b}, (a, b) ∈ t → (b, a) ∈ t) ∧ t ○ t ⊆ s :=
let ⟨_t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
let ⟨t', ht', ht'₁, ht'₂⟩ := symm_of_uniformity ht₁
⟨t', ht', ht'₁ _ _, Subset.trans (monotone_id.compRel monotone_id ht'₂) ht₂⟩
#align comp_symm_of_uniformity comp_symm_of_uniformity
theorem uniformity_le_symm : 𝓤 α ≤ @Prod.swap α α <$> 𝓤 α := by
rw [map_swap_eq_comap_swap]; exact tendsto_swap_uniformity.le_comap
#align uniformity_le_symm uniformity_le_symm
theorem uniformity_eq_symm : 𝓤 α = @Prod.swap α α <$> 𝓤 α :=
le_antisymm uniformity_le_symm symm_le_uniformity
#align uniformity_eq_symm uniformity_eq_symm
@[simp]
theorem comap_swap_uniformity : comap (@Prod.swap α α) (𝓤 α) = 𝓤 α :=
(congr_arg _ uniformity_eq_symm).trans <| comap_map Prod.swap_injective
#align comap_swap_uniformity comap_swap_uniformity
theorem symmetrize_mem_uniformity {V : Set (α × α)} (h : V ∈ 𝓤 α) : symmetrizeRel V ∈ 𝓤 α := by
apply (𝓤 α).inter_sets h
rw [← image_swap_eq_preimage_swap, uniformity_eq_symm]
exact image_mem_map h
#align symmetrize_mem_uniformity symmetrize_mem_uniformity
/-- Symmetric entourages form a basis of `𝓤 α` -/
theorem UniformSpace.hasBasis_symmetric :
(𝓤 α).HasBasis (fun s : Set (α × α) => s ∈ 𝓤 α ∧ SymmetricRel s) id :=
hasBasis_self.2 fun t t_in =>
⟨symmetrizeRel t, symmetrize_mem_uniformity t_in, symmetric_symmetrizeRel t,
symmetrizeRel_subset_self t⟩
#align uniform_space.has_basis_symmetric UniformSpace.hasBasis_symmetric
theorem uniformity_lift_le_swap {g : Set (α × α) → Filter β} {f : Filter β} (hg : Monotone g)
(h : ((𝓤 α).lift fun s => g (preimage Prod.swap s)) ≤ f) : (𝓤 α).lift g ≤ f :=
calc
(𝓤 α).lift g ≤ (Filter.map (@Prod.swap α α) <| 𝓤 α).lift g :=
lift_mono uniformity_le_symm le_rfl
_ ≤ _ := by rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]; exact h
#align uniformity_lift_le_swap uniformity_lift_le_swap
theorem uniformity_lift_le_comp {f : Set (α × α) → Filter β} (h : Monotone f) :
((𝓤 α).lift fun s => f (s ○ s)) ≤ (𝓤 α).lift f :=
calc
((𝓤 α).lift fun s => f (s ○ s)) = ((𝓤 α).lift' fun s : Set (α × α) => s ○ s).lift f := by
rw [lift_lift'_assoc]
exact monotone_id.compRel monotone_id
exact h
_ ≤ (𝓤 α).lift f := lift_mono comp_le_uniformity le_rfl
#align uniformity_lift_le_comp uniformity_lift_le_comp
-- Porting note (#10756): new lemma
theorem comp3_mem_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ (t ○ t) ⊆ s :=
let ⟨_t', ht', ht's⟩ := comp_mem_uniformity_sets hs
let ⟨t, ht, htt'⟩ := comp_mem_uniformity_sets ht'
⟨t, ht, (compRel_mono ((subset_comp_self (refl_le_uniformity ht)).trans htt') htt').trans ht's⟩
/-- See also `comp3_mem_uniformity`. -/
theorem comp_le_uniformity3 : ((𝓤 α).lift' fun s : Set (α × α) => s ○ (s ○ s)) ≤ 𝓤 α := fun _ h =>
let ⟨_t, htU, ht⟩ := comp3_mem_uniformity h
mem_of_superset (mem_lift' htU) ht
#align comp_le_uniformity3 comp_le_uniformity3
/-- See also `comp_open_symm_mem_uniformity_sets`. -/
theorem comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ⊆ s := by
obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs
use symmetrizeRel w, symmetrize_mem_uniformity w_in, symmetric_symmetrizeRel w
have : symmetrizeRel w ⊆ w := symmetrizeRel_subset_self w
calc symmetrizeRel w ○ symmetrizeRel w
_ ⊆ w ○ w := by mono
_ ⊆ s := w_sub
#align comp_symm_mem_uniformity_sets comp_symm_mem_uniformity_sets
theorem subset_comp_self_of_mem_uniformity {s : Set (α × α)} (h : s ∈ 𝓤 α) : s ⊆ s ○ s :=
subset_comp_self (refl_le_uniformity h)
#align subset_comp_self_of_mem_uniformity subset_comp_self_of_mem_uniformity
theorem comp_comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s := by
rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩
rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩
use t, t_in, t_symm
have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in
-- Porting note: Needed the following `have`s to make `mono` work
have ht := Subset.refl t
have hw := Subset.refl w
calc
t ○ t ○ t ⊆ w ○ t := by mono
_ ⊆ w ○ (t ○ t) := by mono
_ ⊆ w ○ w := by mono
_ ⊆ s := w_sub
#align comp_comp_symm_mem_uniformity_sets comp_comp_symm_mem_uniformity_sets
/-!
### Balls in uniform spaces
-/
/-- The ball around `(x : β)` with respect to `(V : Set (β × β))`. Intended to be
used for `V ∈ 𝓤 β`, but this is not needed for the definition. Recovers the
notions of metric space ball when `V = {p | dist p.1 p.2 < r }`. -/
def UniformSpace.ball (x : β) (V : Set (β × β)) : Set β :=
Prod.mk x ⁻¹' V
#align uniform_space.ball UniformSpace.ball
open UniformSpace (ball)
theorem UniformSpace.mem_ball_self (x : α) {V : Set (α × α)} (hV : V ∈ 𝓤 α) : x ∈ ball x V :=
refl_mem_uniformity hV
#align uniform_space.mem_ball_self UniformSpace.mem_ball_self
/-- The triangle inequality for `UniformSpace.ball` -/
theorem mem_ball_comp {V W : Set (β × β)} {x y z} (h : y ∈ ball x V) (h' : z ∈ ball y W) :
z ∈ ball x (V ○ W) :=
prod_mk_mem_compRel h h'
#align mem_ball_comp mem_ball_comp
theorem ball_subset_of_comp_subset {V W : Set (β × β)} {x y} (h : x ∈ ball y W) (h' : W ○ W ⊆ V) :
ball x W ⊆ ball y V := fun _z z_in => h' (mem_ball_comp h z_in)
#align ball_subset_of_comp_subset ball_subset_of_comp_subset
theorem ball_mono {V W : Set (β × β)} (h : V ⊆ W) (x : β) : ball x V ⊆ ball x W :=
preimage_mono h
#align ball_mono ball_mono
theorem ball_inter (x : β) (V W : Set (β × β)) : ball x (V ∩ W) = ball x V ∩ ball x W :=
preimage_inter
#align ball_inter ball_inter
theorem ball_inter_left (x : β) (V W : Set (β × β)) : ball x (V ∩ W) ⊆ ball x V :=
ball_mono (inter_subset_left V W) x
#align ball_inter_left ball_inter_left
theorem ball_inter_right (x : β) (V W : Set (β × β)) : ball x (V ∩ W) ⊆ ball x W :=
ball_mono (inter_subset_right V W) x
#align ball_inter_right ball_inter_right
theorem mem_ball_symmetry {V : Set (β × β)} (hV : SymmetricRel V) {x y} :
x ∈ ball y V ↔ y ∈ ball x V :=
show (x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V by
unfold SymmetricRel at hV
rw [hV]
#align mem_ball_symmetry mem_ball_symmetry
theorem ball_eq_of_symmetry {V : Set (β × β)} (hV : SymmetricRel V) {x} :
ball x V = { y | (y, x) ∈ V } := by
ext y
rw [mem_ball_symmetry hV]
exact Iff.rfl
#align ball_eq_of_symmetry ball_eq_of_symmetry
theorem mem_comp_of_mem_ball {V W : Set (β × β)} {x y z : β} (hV : SymmetricRel V)
(hx : x ∈ ball z V) (hy : y ∈ ball z W) : (x, y) ∈ V ○ W := by
rw [mem_ball_symmetry hV] at hx
exact ⟨z, hx, hy⟩
#align mem_comp_of_mem_ball mem_comp_of_mem_ball
theorem UniformSpace.isOpen_ball (x : α) {V : Set (α × α)} (hV : IsOpen V) : IsOpen (ball x V) :=
hV.preimage <| continuous_const.prod_mk continuous_id
#align uniform_space.is_open_ball UniformSpace.isOpen_ball
theorem UniformSpace.isClosed_ball (x : α) {V : Set (α × α)} (hV : IsClosed V) :
IsClosed (ball x V) :=
hV.preimage <| continuous_const.prod_mk continuous_id
theorem mem_comp_comp {V W M : Set (β × β)} (hW' : SymmetricRel W) {p : β × β} :
p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty := by
cases' p with x y
constructor
· rintro ⟨z, ⟨w, hpw, hwz⟩, hzy⟩
exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry hW']⟩, hwz⟩
· rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩
rw [mem_ball_symmetry hW'] at z_in
exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩
#align mem_comp_comp mem_comp_comp
/-!
### Neighborhoods in uniform spaces
-/
theorem mem_nhds_uniformity_iff_right {x : α} {s : Set α} :
s ∈ 𝓝 x ↔ { p : α × α | p.1 = x → p.2 ∈ s } ∈ 𝓤 α := by
simp only [nhds_eq_comap_uniformity, mem_comap_prod_mk]
#align mem_nhds_uniformity_iff_right mem_nhds_uniformity_iff_right
theorem mem_nhds_uniformity_iff_left {x : α} {s : Set α} :
s ∈ 𝓝 x ↔ { p : α × α | p.2 = x → p.1 ∈ s } ∈ 𝓤 α := by
rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]
simp only [map_def, mem_map, preimage_setOf_eq, Prod.snd_swap, Prod.fst_swap]
#align mem_nhds_uniformity_iff_left mem_nhds_uniformity_iff_left
theorem nhdsWithin_eq_comap_uniformity_of_mem {x : α} {T : Set α} (hx : x ∈ T) (S : Set α) :
𝓝[S] x = (𝓤 α ⊓ 𝓟 (T ×ˢ S)).comap (Prod.mk x) := by
simp [nhdsWithin, nhds_eq_comap_uniformity, hx]
theorem nhdsWithin_eq_comap_uniformity {x : α} (S : Set α) :
𝓝[S] x = (𝓤 α ⊓ 𝓟 (univ ×ˢ S)).comap (Prod.mk x) :=
nhdsWithin_eq_comap_uniformity_of_mem (mem_univ _) S
/-- See also `isOpen_iff_open_ball_subset`. -/
theorem isOpen_iff_ball_subset {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s := by
simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]
#align is_open_iff_ball_subset isOpen_iff_ball_subset
theorem nhds_basis_uniformity' {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s)
{x : α} : (𝓝 x).HasBasis p fun i => ball x (s i) := by
rw [nhds_eq_comap_uniformity]
exact h.comap (Prod.mk x)
#align nhds_basis_uniformity' nhds_basis_uniformity'
theorem nhds_basis_uniformity {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s)
{x : α} : (𝓝 x).HasBasis p fun i => { y | (y, x) ∈ s i } := by
replace h := h.comap Prod.swap
rw [comap_swap_uniformity] at h
exact nhds_basis_uniformity' h
#align nhds_basis_uniformity nhds_basis_uniformity
theorem nhds_eq_comap_uniformity' {x : α} : 𝓝 x = (𝓤 α).comap fun y => (y, x) :=
(nhds_basis_uniformity (𝓤 α).basis_sets).eq_of_same_basis <| (𝓤 α).basis_sets.comap _
#align nhds_eq_comap_uniformity' nhds_eq_comap_uniformity'
theorem UniformSpace.mem_nhds_iff {x : α} {s : Set α} : s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s := by
rw [nhds_eq_comap_uniformity, mem_comap]
simp_rw [ball]
#align uniform_space.mem_nhds_iff UniformSpace.mem_nhds_iff
theorem UniformSpace.ball_mem_nhds (x : α) ⦃V : Set (α × α)⦄ (V_in : V ∈ 𝓤 α) : ball x V ∈ 𝓝 x := by
rw [UniformSpace.mem_nhds_iff]
exact ⟨V, V_in, Subset.rfl⟩
#align uniform_space.ball_mem_nhds UniformSpace.ball_mem_nhds
theorem UniformSpace.ball_mem_nhdsWithin {x : α} {S : Set α} ⦃V : Set (α × α)⦄ (x_in : x ∈ S)
(V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)) : ball x V ∈ 𝓝[S] x := by
rw [nhdsWithin_eq_comap_uniformity_of_mem x_in, mem_comap]
exact ⟨V, V_in, Subset.rfl⟩
theorem UniformSpace.mem_nhds_iff_symm {x : α} {s : Set α} :
s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ ball x V ⊆ s := by
rw [UniformSpace.mem_nhds_iff]
constructor
· rintro ⟨V, V_in, V_sub⟩
use symmetrizeRel V, symmetrize_mem_uniformity V_in, symmetric_symmetrizeRel V
exact Subset.trans (ball_mono (symmetrizeRel_subset_self V) x) V_sub
· rintro ⟨V, V_in, _, V_sub⟩
exact ⟨V, V_in, V_sub⟩
#align uniform_space.mem_nhds_iff_symm UniformSpace.mem_nhds_iff_symm
theorem UniformSpace.hasBasis_nhds (x : α) :
HasBasis (𝓝 x) (fun s : Set (α × α) => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s :=
⟨fun t => by simp [UniformSpace.mem_nhds_iff_symm, and_assoc]⟩
#align uniform_space.has_basis_nhds UniformSpace.hasBasis_nhds
open UniformSpace
theorem UniformSpace.mem_closure_iff_symm_ball {s : Set α} {x} :
x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → SymmetricRel V → (s ∩ ball x V).Nonempty := by
simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]
#align uniform_space.mem_closure_iff_symm_ball UniformSpace.mem_closure_iff_symm_ball
theorem UniformSpace.mem_closure_iff_ball {s : Set α} {x} :
x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty := by
simp [mem_closure_iff_nhds_basis' (nhds_basis_uniformity' (𝓤 α).basis_sets)]
#align uniform_space.mem_closure_iff_ball UniformSpace.mem_closure_iff_ball
theorem UniformSpace.hasBasis_nhds_prod (x y : α) :
HasBasis (𝓝 (x, y)) (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s := by
rw [nhds_prod_eq]
apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)
rintro U V ⟨U_in, U_symm⟩ ⟨V_in, V_symm⟩
exact
⟨U ∩ V, ⟨(𝓤 α).inter_sets U_in V_in, U_symm.inter V_symm⟩, ball_inter_left x U V,
ball_inter_right y U V⟩
#align uniform_space.has_basis_nhds_prod UniformSpace.hasBasis_nhds_prod
theorem nhds_eq_uniformity {x : α} : 𝓝 x = (𝓤 α).lift' (ball x) :=
(nhds_basis_uniformity' (𝓤 α).basis_sets).eq_biInf
#align nhds_eq_uniformity nhds_eq_uniformity
theorem nhds_eq_uniformity' {x : α} : 𝓝 x = (𝓤 α).lift' fun s => { y | (y, x) ∈ s } :=
(nhds_basis_uniformity (𝓤 α).basis_sets).eq_biInf
#align nhds_eq_uniformity' nhds_eq_uniformity'
theorem mem_nhds_left (x : α) {s : Set (α × α)} (h : s ∈ 𝓤 α) : { y : α | (x, y) ∈ s } ∈ 𝓝 x :=
ball_mem_nhds x h
#align mem_nhds_left mem_nhds_left
theorem mem_nhds_right (y : α) {s : Set (α × α)} (h : s ∈ 𝓤 α) : { x : α | (x, y) ∈ s } ∈ 𝓝 y :=
mem_nhds_left _ (symm_le_uniformity h)
#align mem_nhds_right mem_nhds_right
theorem exists_mem_nhds_ball_subset_of_mem_nhds {a : α} {U : Set α} (h : U ∈ 𝓝 a) :
∃ V ∈ 𝓝 a, ∃ t ∈ 𝓤 α, ∀ a' ∈ V, UniformSpace.ball a' t ⊆ U :=
let ⟨t, ht, htU⟩ := comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 h)
⟨_, mem_nhds_left a ht, t, ht, fun a₁ h₁ a₂ h₂ => @htU (a, a₂) ⟨a₁, h₁, h₂⟩ rfl⟩
#align exists_mem_nhds_ball_subset_of_mem_nhds exists_mem_nhds_ball_subset_of_mem_nhds
theorem tendsto_right_nhds_uniformity {a : α} : Tendsto (fun a' => (a', a)) (𝓝 a) (𝓤 α) := fun _ =>
mem_nhds_right a
#align tendsto_right_nhds_uniformity tendsto_right_nhds_uniformity
theorem tendsto_left_nhds_uniformity {a : α} : Tendsto (fun a' => (a, a')) (𝓝 a) (𝓤 α) := fun _ =>
mem_nhds_left a
#align tendsto_left_nhds_uniformity tendsto_left_nhds_uniformity
theorem lift_nhds_left {x : α} {g : Set α → Filter β} (hg : Monotone g) :
(𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g (ball x s) := by
rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]
simp_rw [ball, Function.comp]
#align lift_nhds_left lift_nhds_left
theorem lift_nhds_right {x : α} {g : Set α → Filter β} (hg : Monotone g) :
(𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g { y | (y, x) ∈ s } := by
rw [nhds_eq_comap_uniformity', comap_lift_eq2 hg]
simp_rw [Function.comp, preimage]
#align lift_nhds_right lift_nhds_right
theorem nhds_nhds_eq_uniformity_uniformity_prod {a b : α} :
𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s : Set (α × α) =>
(𝓤 α).lift' fun t => { y : α | (y, a) ∈ s } ×ˢ { y : α | (b, y) ∈ t } := by
rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
exacts [rfl, monotone_preimage, monotone_preimage]
#align nhds_nhds_eq_uniformity_uniformity_prod nhds_nhds_eq_uniformity_uniformity_prod
theorem nhds_eq_uniformity_prod {a b : α} :
𝓝 (a, b) =
(𝓤 α).lift' fun s : Set (α × α) => { y : α | (y, a) ∈ s } ×ˢ { y : α | (b, y) ∈ s } := by
rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']
· exact fun s => monotone_const.set_prod monotone_preimage
· refine fun t => Monotone.set_prod ?_ monotone_const
exact monotone_preimage (f := fun y => (y, a))
#align nhds_eq_uniformity_prod nhds_eq_uniformity_prod
theorem nhdset_of_mem_uniformity {d : Set (α × α)} (s : Set (α × α)) (hd : d ∈ 𝓤 α) :
∃ t : Set (α × α), IsOpen t ∧ s ⊆ t ∧
t ⊆ { p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d } := by
let cl_d := { p : α × α | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d }
have : ∀ p ∈ s, ∃ t, t ⊆ cl_d ∧ IsOpen t ∧ p ∈ t := fun ⟨x, y⟩ hp =>
mem_nhds_iff.mp <|
show cl_d ∈ 𝓝 (x, y) by
rw [nhds_eq_uniformity_prod, mem_lift'_sets]
· exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
· exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
choose t ht using this
exact ⟨(⋃ p : α × α, ⋃ h : p ∈ s, t p h : Set (α × α)),
isOpen_iUnion fun p : α × α => isOpen_iUnion fun hp => (ht p hp).right.left,
fun ⟨a, b⟩ hp => by
simp only [mem_iUnion, Prod.exists]; exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩,
iUnion_subset fun p => iUnion_subset fun hp => (ht p hp).left⟩
#align nhdset_of_mem_uniformity nhdset_of_mem_uniformity
/-- Entourages are neighborhoods of the diagonal. -/
theorem nhds_le_uniformity (x : α) : 𝓝 (x, x) ≤ 𝓤 α := by
intro V V_in
rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩
have : ball x w ×ˢ ball x w ∈ 𝓝 (x, x) := by
rw [nhds_prod_eq]
exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)
apply mem_of_superset this
rintro ⟨u, v⟩ ⟨u_in, v_in⟩
exact w_sub (mem_comp_of_mem_ball w_symm u_in v_in)
#align nhds_le_uniformity nhds_le_uniformity
/-- Entourages are neighborhoods of the diagonal. -/
theorem iSup_nhds_le_uniformity : ⨆ x : α, 𝓝 (x, x) ≤ 𝓤 α :=
iSup_le nhds_le_uniformity
#align supr_nhds_le_uniformity iSup_nhds_le_uniformity
/-- Entourages are neighborhoods of the diagonal. -/
theorem nhdsSet_diagonal_le_uniformity : 𝓝ˢ (diagonal α) ≤ 𝓤 α :=
(nhdsSet_diagonal α).trans_le iSup_nhds_le_uniformity
#align nhds_set_diagonal_le_uniformity nhdsSet_diagonal_le_uniformity
/-!
### Closure and interior in uniform spaces
-/
theorem closure_eq_uniformity (s : Set <| α × α) :
closure s = ⋂ V ∈ { V | V ∈ 𝓤 α ∧ SymmetricRel V }, V ○ s ○ V := by
ext ⟨x, y⟩
simp (config := { contextual := true }) only
[mem_closure_iff_nhds_basis (UniformSpace.hasBasis_nhds_prod x y), mem_iInter, mem_setOf_eq,
and_imp, mem_comp_comp, exists_prop, ← mem_inter_iff, inter_comm, Set.Nonempty]
#align closure_eq_uniformity closure_eq_uniformity
theorem uniformity_hasBasis_closed :
HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α ∧ IsClosed V) id := by
refine' Filter.hasBasis_self.2 fun t h => _
rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩
refine' ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, _⟩
refine' Subset.trans _ r
rw [closure_eq_uniformity]
apply iInter_subset_of_subset
apply iInter_subset
exact ⟨w_in, w_symm⟩
#align uniformity_has_basis_closed uniformity_hasBasis_closed
theorem uniformity_eq_uniformity_closure : 𝓤 α = (𝓤 α).lift' closure :=
Eq.symm <| uniformity_hasBasis_closed.lift'_closure_eq_self fun _ => And.right
#align uniformity_eq_uniformity_closure uniformity_eq_uniformity_closure
theorem Filter.HasBasis.uniformity_closure {p : ι → Prop} {U : ι → Set (α × α)}
(h : (𝓤 α).HasBasis p U) : (𝓤 α).HasBasis p fun i => closure (U i) :=
(@uniformity_eq_uniformity_closure α _).symm ▸ h.lift'_closure
#align filter.has_basis.uniformity_closure Filter.HasBasis.uniformity_closure
/-- Closed entourages form a basis of the uniformity filter. -/
theorem uniformity_hasBasis_closure : HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α) closure :=
(𝓤 α).basis_sets.uniformity_closure
#align uniformity_has_basis_closure uniformity_hasBasis_closure
theorem closure_eq_inter_uniformity {t : Set (α × α)} : closure t = ⋂ d ∈ 𝓤 α, d ○ (t ○ d) :=
calc
closure t = ⋂ (V) (_ : V ∈ 𝓤 α ∧ SymmetricRel V), V ○ t ○ V := closure_eq_uniformity t
_ = ⋂ V ∈ 𝓤 α, V ○ t ○ V :=
Eq.symm <|
UniformSpace.hasBasis_symmetric.biInter_mem fun V₁ V₂ hV =>
compRel_mono (compRel_mono hV Subset.rfl) hV
_ = ⋂ V ∈ 𝓤 α, V ○ (t ○ V) := by simp only [compRel_assoc]
#align closure_eq_inter_uniformity closure_eq_inter_uniformity
theorem uniformity_eq_uniformity_interior : 𝓤 α = (𝓤 α).lift' interior :=
le_antisymm
(le_iInf₂ fun d hd => by
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
have : s ⊆ interior d :=
calc
s ⊆ t := hst
_ ⊆ interior d :=
ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
hs_comp ⟨x, h₁, y, h₂, h₃⟩
have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this
simp [this])
fun s hs => ((𝓤 α).lift' interior).sets_of_superset (mem_lift' hs) interior_subset
#align uniformity_eq_uniformity_interior uniformity_eq_uniformity_interior
theorem interior_mem_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) : interior s ∈ 𝓤 α := by
rw [uniformity_eq_uniformity_interior]; exact mem_lift' hs
#align interior_mem_uniformity interior_mem_uniformity
theorem mem_uniformity_isClosed {s : Set (α × α)} (h : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, IsClosed t ∧ t ⊆ s :=
let ⟨t, ⟨ht_mem, htc⟩, hts⟩ := uniformity_hasBasis_closed.mem_iff.1 h
⟨t, ht_mem, htc, hts⟩
#align mem_uniformity_is_closed mem_uniformity_isClosed
theorem isOpen_iff_open_ball_subset {s : Set α} :
IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s := by
rw [isOpen_iff_ball_subset]
constructor <;> intro h x hx
· obtain ⟨V, hV, hV'⟩ := h x hx
exact
⟨interior V, interior_mem_uniformity hV, isOpen_interior,
(ball_mono interior_subset x).trans hV'⟩
· obtain ⟨V, hV, -, hV'⟩ := h x hx
exact ⟨V, hV, hV'⟩
#align is_open_iff_open_ball_subset isOpen_iff_open_ball_subset
/-- The uniform neighborhoods of all points of a dense set cover the whole space. -/