complete_of_finiteDimensional — Mathlib

English

If s is a subspace of E that is finite-dimensional (as a 𝕜-vector space), then s is a complete subset of E.

Русский

Если s — субпространство E и оно конечномерно, то как подпространство оно полно относительно нормированной структуры пространства.

LaTeX

$$$\\text{FiniteDimensional}_{𝕜} (s) \\Rightarrow \\text{IsComplete } (s \\subseteq E)$$$

Lean4

/-- A finite-dimensional subspace is complete. -/
theorem complete_of_finiteDimensional (s : Submodule 𝕜 E) [FiniteDimensional 𝕜 s] : IsComplete (s : Set E) :=
  haveI : IsUniformAddGroup s := s.toAddSubgroup.isUniformAddGroup
  completeSpace_coe_iff_isComplete.1 (FiniteDimensional.complete 𝕜 s)

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