isBounded

Mathlib.Topology.MetricSpace.Bounded

URI: https://scilib.ai/kg/mathlib#IsCompact.isBounded

← MathLib Explorer

English

IsCompact s implies IsBounded s.

Русский

Компактность множества означает его ограниченность.

LaTeX

$$$IsCompact\; s \Rightarrow IsBounded\; s$$$

Lean4

/-- A compact set is bounded -/
@[aesop 50% apply, grind ←]
theorem _root_.IsCompact.isBounded {s : Set α} (h : IsCompact s) : IsBounded s :=
  -- A compact set is totally bounded, thus bounded

  h.totallyBounded.isBounded

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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