isPartition_splitCenter

Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

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

English

The center split prepartition is a partition.

Русский

Центрированное разбиение является разбиением.

LaTeX

$$$ \\text{IsPartition}(\\mathrm{splitCenter}(I)) $$$

Lean4

theorem isPartition_splitCenter (I : Box ι) : IsPartition (splitCenter I) := fun x hx => by simp [hx]

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

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

Разделы

Аффилиация

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