splitUpper_le

Mathlib.Analysis.BoxIntegral.Partition.Split

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

English

I.splitUpper i x ≤ I.

Русский

I.splitUpper i x ≤ I.

LaTeX

$$$I.splitUpper i x \\le I$$$

Lean4

theorem splitUpper_le : I.splitUpper i x ≤ I :=
  withBotCoe_subset_iff.1 <| by simp

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

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

Разделы

Аффилиация

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