isBounded_Icc

Mathlib.Analysis.BoxIntegral.Box.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Box.isBounded_Icc

English

The closed box Box.Icc I is compact.

Русский

Замкнутый короб Box.Icc I компактен.

LaTeX

$$$ IsCompact(Box.Icc I) $$$

Lean4

theorem isBounded_Icc [Finite ι] (I : Box ι) : Bornology.IsBounded (Box.Icc I) :=
  by
  cases nonempty_fintype ι
  exact Metric.isBounded_Icc _ _

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

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

Разделы

Аффилиация

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