Theorems · Theorem · real analysis

BoxIntegral.Prepartition.exists_iUnion_eq_sdiff

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [Finite ι] (π : BoxIntegral.Prepartition I), ∃ π', π'.iUnion = ↑I \ π.iUnion

For every prepartition π of I there exists a prepartition that covers exactly I \ π.iUnion.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Split

Cited by

3 results in Mathlib

Foundations

Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Finite