splitMany_le_split

Mathlib.Analysis.BoxIntegral.Partition.Split

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.splitMany_le_split

English

If p ∈ s, then splitMany I s ≤ split I p.1 p.2.

Русский

Если p принадлежит s, то splitMany I s ≤ split I p.1 p.2.

LaTeX

$$$splitMany\\ I\\ s \\leq split I p.1 p.2$$$

Lean4

theorem splitMany_le_split (I : Box ι) {s : Finset (ι × ℝ)} {p : ι × ℝ} (hp : p ∈ s) :
    splitMany I s ≤ split I p.1 p.2 :=
  Finset.inf_le hp

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

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

Разделы

Аффилиация

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