-
Notifications
You must be signed in to change notification settings - Fork 297
/
completion.lean
52 lines (40 loc) · 1.42 KB
/
completion.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
/-
Copyright (c) 2021 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin
-/
import analysis.normed.group.basic
import topology.algebra.group_completion
import topology.metric_space.completion
/-!
# Completion of a normed group
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that the completion of a (semi)normed group is a normed group.
## Tags
normed group, completion
-/
noncomputable theory
namespace uniform_space
namespace completion
variables (E : Type*)
instance [uniform_space E] [has_norm E] :
has_norm (completion E) :=
{ norm := completion.extension has_norm.norm }
@[simp] lemma norm_coe {E} [seminormed_add_comm_group E] (x : E) :
‖(x : completion E)‖ = ‖x‖ :=
completion.extension_coe uniform_continuous_norm x
instance [seminormed_add_comm_group E] : normed_add_comm_group (completion E) :=
{ dist_eq :=
begin
intros x y,
apply completion.induction_on₂ x y; clear x y,
{ refine is_closed_eq (completion.uniform_continuous_extension₂ _).continuous _,
exact continuous.comp completion.continuous_extension continuous_sub },
{ intros x y,
rw [← completion.coe_sub, norm_coe, completion.dist_eq, dist_eq_norm] }
end,
.. completion.add_comm_group,
.. completion.metric_space }
end completion
end uniform_space