completeSpace — Mathlib

English

If L/K is finite dimensional and K is complete, then L is complete with respect to the spectral-norm-induced uniform structure.

Русский

Если L/K конечномерно и K полноценно, то L является полным относительно униформной структуры, вызываемой спектральной нормой.

LaTeX

$$$\text{CompleteSpace}(L)\;\text{assuming}\; \text{CompleteSpace}(K)\;\text{and}\; \dim_K L < \infty$$$

Lean4

/-- If `L/K` is finite dimensional, then `L` is a complete space with respect to topology induced
  by the spectral norm. -/
instance (priority := 100) completeSpace [CompleteSpace K] [h_fin : FiniteDimensional K L] :
    @CompleteSpace L (uniformSpace K L) := by
  letI := (normedAddCommGroup K L)
  letI := (normedSpace K L)
  exact FiniteDimensional.complete K L

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