Theorems · Theorem · functional analysis

ContinuousLinearMap.fromCompletion_unique

∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  [inst_12 : T0Space β] [inst_13 : CompleteSpace β] (f : α →SL[σ] β) (g : UniformSpace.Completion α →SL[σ] β),
  (∀ (e : α), f e = g ↑e) → f.fromCompletion = g

Defined in

Mathlib.Topology.Algebra.LinearMapCompletion

Cited by

0 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpaceAddCommGroupIsUniformAddGroupSemiringModuleUniformContinuousConstSMulSemiringUniformSpaceAddCommGroupIsUniformAddGroupModuleUniformContinuousConstSMulT0SpaceCompleteSpace