instCompleteSpace — Mathlib

English

Under standard coherence assumptions, the type of continuous linear maps E →SL[σ] F forms a complete space when F is complete and the domain E satisfies topological additivity.

Русский

При стандартных предпосылках когерентности множество непрерывных линейных отображений E →SL[σ] F образует полное пространство, если F полно, а область E удовлетворяет условиям топологического дополнения.

LaTeX

$$$IsCoherentWith\\{s : Set E | IsVonNBounded 𝕜_1 s\\} \\\Rightarrow CompleteSpace(E →SL[σ] F)$$$

Lean4

instance instCompleteSpace [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [SequentialSpace E] [UniformSpace F]
    [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] : CompleteSpace (E →SL[σ] F) :=
  completeSpace <| .of_seq fun _ _ h ↦ (h.isVonNBounded_range 𝕜₁).insert _

Похожие утверждения