proper_real — Mathlib

English

A finite-dimensional normed real vector space E is a proper space (with the standard structures).

Русский

Конечномерное нормированное вещественное пространство E является корректным.

LaTeX

$$$[FiniteDimensional \\; \\mathbb{R} E] \\\\Rightarrow ProperSpace E$$$

Lean4

instance (priority := 900) proper_real (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] :
    ProperSpace E :=
  FiniteDimensional.proper ℝ E

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