iUnion_toPrepartition — Mathlib

English

Let π be a TaggedPrepartition of I. The union of boxes obtained by passing π to its associated prepartition is exactly the same as the original union, i.e., the iUnion is preserved under the toPrepartition operation.

Русский

Пусть π — тэггированное разбиение I. Объединение коробок, получаемое переходом π к предразбиению, равно исходному объединению: iUnion сохраняется при переходе к toPrepartition.

LaTeX

$$$ \\operatorname{iUnion}(\\pi^{\\mathrm{toPrepartition}}) = \\operatorname{iUnion}(\\pi) $$$

Lean4

@[simp]
theorem iUnion_toPrepartition : π.toPrepartition.iUnion = π.iUnion :=
  rfl

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