noncompactSpace

Mathlib.Analysis.Normed.Module.Basic

URI: https://scilib.ai/kg/mathlib#RealNormedSpace.noncompactSpace

English

If E is a normed space over ℝ, then E is noncompact.

Русский

Если E — нормированное пространство над ℝ, то E не является компактным.

LaTeX

$$$\\mathrm{NoncompactSpace}(E)$$$

Lean4

instance (priority := 100) noncompactSpace [NormedSpace ℝ E] : NoncompactSpace E :=
  NormedSpace.noncompactSpace ℝ E

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru