properSpace_submodule — Mathlib

English

If S is a submodule S of E over a field K with [RCLike K] and FiniteDimensional K S, then S is a proper metric space.

Русский

Если S — подпространство E над полем K (K — RCLike) и [FiniteDimensional K S], то S является правильным метрическим пространством.

LaTeX

$$$[FiniteDimensional_{K} S] \\Rightarrow \\operatorname{ProperSpace} S$$$

Lean4

instance properSpace_submodule (S : Submodule K E) [FiniteDimensional K S] : ProperSpace S :=
  proper_rclike K S

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