isBounded

Mathlib.Analysis.BoxIntegral.Box.Basic

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

English

[Finite ι] Box.Icc I is bounded.

Русский

[Finite ι] Box.Icc I ограничен.

LaTeX

$$$ [Finite ι] \\; Box.Icc I \\text{ is bounded} $$$

Lean4

theorem isBounded [Finite ι] (I : Box ι) : Bornology.IsBounded I.toSet :=
  Bornology.IsBounded.subset I.isBounded_Icc coe_subset_Icc

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

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

Разделы

Аффилиация

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