English
A set s is an entourage in the completion iff there exists ε>0 such that whenever dist a b < ε, then (a,b) ∈ s.
Русский
Множество s является окружением в завершении тогда и только тогда, когда существует ε>0 такое, что для любых a,b, если dist a b < ε, то (a,b) ∈ s.
LaTeX
$$$s\in \mathcal{U}(\mathrm{Completion}\,\alpha) \iff \exists \varepsilon>0, \forall {a,b}, \operatorname{dist} a b < \varepsilon \Rightarrow (a,b)\in s$$$
Lean4
/-- Elements of the uniformity (defined generally for completions) can be characterized in terms
of the distance. -/
protected theorem mem_uniformity_dist (s : Set (Completion α × Completion α)) :
s ∈ 𝓤 (Completion α) ↔ ∃ ε > 0, ∀ {a b}, dist a b < ε → (a, b) ∈ s :=
by
constructor
· /- Start from an entourage `s`. It contains a closed entourage `t`. Its pullback in `α` is an
entourage, so it contains an `ε`-neighborhood of the diagonal by definition of the entourages
in metric spaces. Then `t` contains an `ε`-neighborhood of the diagonal in `Completion α`, as
closed properties pass to the completion. -/
intro hs
rcases mem_uniformity_isClosed hs with ⟨t, ht, ⟨tclosed, ts⟩⟩
have A : {x : α × α | (↑x.1, ↑x.2) ∈ t} ∈ uniformity α := uniformContinuous_def.1 (uniformContinuous_coe α) t ht
rcases mem_uniformity_dist.1 A with ⟨ε, εpos, hε⟩
refine ⟨ε, εpos, @fun x y hxy ↦ ?_⟩
have : ε ≤ dist x y ∨ (x, y) ∈ t := by
refine induction_on₂ x y ?_ ?_
· have :
{x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} =
{p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t :=
by ext; simp
rw [this]
apply IsClosed.union _ tclosed
exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
· intro x y
rw [Completion.dist_eq]
by_cases h : ε ≤ dist x y
· exact Or.inl h
· have Z := hε (not_le.1 h)
simp only [Set.mem_setOf_eq] at Z
exact Or.inr Z
simp only [not_le.mpr hxy, false_or] at this
exact ts this
· /- Start from a set `s` containing an ε-neighborhood of the diagonal in `Completion α`. To show
that it is an entourage, we use the fact that `dist` is uniformly continuous on
`Completion α × Completion α` (this is a general property of the extension of uniformly
continuous functions). Therefore, the preimage of the ε-neighborhood of the diagonal in ℝ
is an entourage in `Completion α × Completion α`. Massaging this property, it follows that
the ε-neighborhood of the diagonal is an entourage in `Completion α`, and therefore this is
also the case of `s`. -/
rintro ⟨ε, εpos, hε⟩
let r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos
have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this
simp only [uniformity_prod_eq_prod, mem_prod_iff, Filter.mem_map] at T
rcases T with ⟨t1, ht1, t2, ht2, ht⟩
refine mem_of_superset ht1 ?_
have A : ∀ a b : Completion α, (a, b) ∈ t1 → dist a b < ε :=
by
intro a b hab
have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
exact
lt_of_le_of_lt (le_abs_self _)
(by simpa [r, Completion.dist_self, Real.dist_eq, Completion.dist_comm] using ht this)
grind
