Mathlib.Analysis.Normed.Group.Completion

Module docstring

{"# Completion of a normed group

In this file we prove that the completion of a (semi)normed group is a normed group.

Tags

normed group, completion "}

UniformSpace.Completion.instNorm instance

[UniformSpace E] [Norm E] : Norm (Completion E)

Full source

instance [UniformSpace E] [Norm E] : Norm (Completion E) where
  norm := Completion.extension Norm.norm

Norm Structure on the Completion of a Normed Space

Informal description

For any uniform space $E$ equipped with a norm $\|\cdot\|$, the completion of $E$ inherits a norm structure. Specifically, the norm on the completion $\text{Completion}(E)$ is defined in such a way that it extends the original norm on $E$.

UniformSpace.Completion.norm_coe theorem

{E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖ = ‖x‖

Full source

@[simp]
theorem norm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖ = ‖x‖ :=
  Completion.extension_coe uniformContinuous_norm x

Norm Preservation in Completion of Seminormed Group

Informal description

For any element $x$ in a seminormed additive commutative group $E$, the norm of $x$ in the completion $\overline{E}$ of $E$ is equal to the norm of $x$ in $E$, i.e., $\|x\|_{\overline{E}} = \|x\|_E$.

UniformSpace.Completion.instNormedAddCommGroup instance

[SeminormedAddCommGroup E] : NormedAddCommGroup (Completion E)

Full source

instance [SeminormedAddCommGroup E] : NormedAddCommGroup (Completion E) where
  dist_eq x y := by
    induction x, y using Completion.induction_on₂
    · refine isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_
      exact Continuous.comp Completion.continuous_extension continuous_sub
    · rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]

Completion of a Seminormed Group is a Normed Group

Informal description

For any seminormed additive commutative group $E$, the completion $\overline{E}$ of $E$ is a normed additive commutative group. The norm on $\overline{E}$ extends the norm on $E$, and the metric structure is induced by this norm.

UniformSpace.Completion.nnnorm_coe theorem

{E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖₊ = ‖x‖₊

Full source

@[simp]
theorem nnnorm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖₊ = ‖x‖₊ := by
  simp [nnnorm]

Seminorm Preservation in Completion of Seminormed Group

Informal description

For any element $x$ in a seminormed additive commutative group $E$, the seminorm of $x$ in the completion $\overline{E}$ of $E$ is equal to the seminorm of $x$ in $E$, i.e., $\|x\|_{\overline{E}} = \|x\|_E$.

UniformSpace.Completion.enorm_coe theorem

{E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖ₑ = ‖x‖ₑ

Full source

@[simp]
lemma enorm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖ₑ = ‖x‖ₑ := by
  simp [enorm]

Extended Norm Preservation in Completion of Seminormed Group

Informal description

For any element $x$ in a seminormed additive commutative group $E$, the extended norm of $x$ in the completion $\overline{E}$ of $E$ is equal to the extended norm of $x$ in $E$, i.e., $\|x\|_{\overline{E}} = \|x\|_E$.