isPartition_iff_iUnion_eq

Mathlib.Analysis.BoxIntegral.Partition.Tagged

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

English

A prepartition π is a partition if and only if its iUnion equals the ambient box I.

Русский

Разбиение π является разбиением, если и только если iUnion(π) совпадает с внешним box I.

LaTeX

$$$ IsPartition(\\pi) \\iff \\pi.iUnion = I $$$

Lean4

theorem isPartition_iff_iUnion_eq : IsPartition π ↔ π.iUnion = I :=
  Prepartition.isPartition_iff_iUnion_eq

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

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

Разделы

Аффилиация

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