isPartition_single

Mathlib.Analysis.BoxIntegral.Partition.Tagged

URI: https://scilib.ai/kg/mathlib#BoxIntegral.TaggedPrepartition.isPartition_single

English

For any x ∈ Box.Icc I, the singleton prepartition with J = I is a partition.

Русский

Для любого x ∈ Box.Icc I одинарное предразбиение с J = I является разбиением.

LaTeX

$$$\text{IsPartition} (single\ I\ I\ le\_rfl\ x\ h)$$$

Lean4

theorem isPartition_single (h : x ∈ Box.Icc I) : (single I I le_rfl x h).IsPartition :=
  Prepartition.isPartitionTop I

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

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

Разделы

Аффилиация

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