splitCenterBox_le

Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

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

English

For any box I and subset s, the splitCenterBox s is contained in I.

Русский

Для любой коробки I и множества s, I.splitCenterBox s содержится в I.

LaTeX

$$$$I.splitCenterBox s \le I.$$$$

Lean4

theorem splitCenterBox_le (I : Box ι) (s : Set ι) : I.splitCenterBox s ≤ I := fun _ hx ↦ (mem_splitCenterBox.1 hx).1

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

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

Разделы

Аффилиация

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