Partitions of rectangular boxes in ℝⁿ

In this file we define (pre)partitions of rectangular boxes in ℝⁿ. A partition of a box I in ℝⁿ (see BoxIntegral.Prepartition and BoxIntegral.Prepartition.IsPartition) is a finite set of pairwise disjoint boxes such that their union is exactly I. We use boxes : Finset (Box ι) to store the set of boxes.

Many lemmas about box integrals deal with pairwise disjoint collections of subboxes, so we define a structure BoxIntegral.Prepartition (I : BoxIntegral.Box ι) that stores a collection of boxes such that

• each box J ∈ boxes is a subbox of I;
• the boxes are pairwise disjoint as sets in ℝⁿ.

Then we define a predicate BoxIntegral.Prepartition.IsPartition; π.IsPartition means that the boxes of π actually cover the whole I. We also define some operations on prepartitions:

• BoxIntegral.Prepartition.biUnion: split each box of a partition into smaller boxes;
• BoxIntegral.Prepartition.restrict: restrict a partition to a smaller box.

We also define a SemilatticeInf structure on BoxIntegral.Prepartition I for all I : BoxIntegral.Box ι.

Tags

rectangular box, partition

structure BoxIntegral.Prepartition {ι : Type u_1} (I : BoxIntegral.Box ι) : Type u_1

A prepartition of I : BoxIntegral.Box ι is a finite set of pairwise disjoint subboxes of I.

• boxes : Finset (BoxIntegral.Box ι)
• le_of_mem' : ∀ J ∈ self.boxes, J ≤ I
• pairwiseDisjoint : Set.Pairwise (↑self.boxes) (Disjoint on BoxIntegral.Box.toSet)

instance BoxIntegral.Prepartition.instMembershipBoxPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : Membership (BoxIntegral.Box ι) (BoxIntegral.Prepartition I)

Equations

• BoxIntegral.Prepartition.instMembershipBoxPrepartition = { mem := fun (J : BoxIntegral.Box ι) (π : BoxIntegral.Prepartition I) => J ∈ π.boxes }

@[simp]

theorem BoxIntegral.Prepartition.mem_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : J ∈ π.boxes ↔ J ∈ π

@[simp]

theorem BoxIntegral.Prepartition.mem_mk {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {s : Finset (BoxIntegral.Box ι)} {h₁ : ∀ J ∈ s, J ≤ I} {h₂ : Set.Pairwise (↑s) (Disjoint on BoxIntegral.Box.toSet)} : J ∈ { boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ } ↔ J ∈ s

theorem BoxIntegral.Prepartition.disjoint_coe_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} {J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h₁ : J₁ ∈ π) (h₂ : J₂ ∈ π) (h : J₁ ≠ J₂) : Disjoint ↑J₁ ↑J₂

theorem BoxIntegral.Prepartition.eq_of_mem_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} {J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι → ℝ} (h₁ : J₁ ∈ π) (h₂ : J₂ ∈ π) (hx₁ : x ∈ J₁) (hx₂ : x ∈ J₂) : J₁ = J₂

theorem BoxIntegral.Prepartition.eq_of_le_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} {J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h₁ : J₁ ∈ π) (h₂ : J₂ ∈ π) (hle₁ : J ≤ J₁) (hle₂ : J ≤ J₂) : J₁ = J₂

theorem BoxIntegral.Prepartition.eq_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} {J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h₁ : J₁ ∈ π) (h₂ : J₂ ∈ π) (hle : J₁ ≤ J₂) : J₁ = J₂

theorem BoxIntegral.Prepartition.le_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (hJ : J ∈ π) : J ≤ I

theorem BoxIntegral.Prepartition.lower_le_lower {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (hJ : J ∈ π) : I.lower ≤ J.lower

theorem BoxIntegral.Prepartition.upper_le_upper {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (hJ : J ∈ π) : J.upper ≤ I.upper

theorem BoxIntegral.Prepartition.injective_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} : Function.Injective BoxIntegral.Prepartition.boxes

theorem BoxIntegral.Prepartition.ext {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : ∀ (J : BoxIntegral.Box ι), J ∈ π₁ ↔ J ∈ π₂) : π₁ = π₂

@[simp]

theorem BoxIntegral.Prepartition.single_boxes {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (h : J ≤ I) : (BoxIntegral.Prepartition.single I J h).boxes = {J}

def BoxIntegral.Prepartition.single {ι : Type u_1} (I : BoxIntegral.Box ι) (J : BoxIntegral.Box ι) (h : J ≤ I) : BoxIntegral.Prepartition I

The singleton prepartition {J}, J ≤ I.

Equations

• BoxIntegral.Prepartition.single I J h = { boxes := {J}, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[simp]

theorem BoxIntegral.Prepartition.mem_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {J' : BoxIntegral.Box ι} (h : J ≤ I) : J' ∈ BoxIntegral.Prepartition.single I J h ↔ J' = J

instance BoxIntegral.Prepartition.instLEPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : LE (BoxIntegral.Prepartition I)

We say that π ≤ π' if each box of π is a subbox of some box of π'.

Equations

• BoxIntegral.Prepartition.instLEPrepartition = { le := fun (π π' : BoxIntegral.Prepartition I) => ∀ ⦃I_1 : BoxIntegral.Box ι⦄, I_1 ∈ π → ∃ I' ∈ π', I_1 ≤ I' }

instance BoxIntegral.Prepartition.partialOrder {ι : Type u_1} {I : BoxIntegral.Box ι} : PartialOrder (BoxIntegral.Prepartition I)

Equations

• BoxIntegral.Prepartition.partialOrder = PartialOrder.mk ⋯

instance BoxIntegral.Prepartition.instOrderTopPrepartitionInstLEPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : OrderTop (BoxIntegral.Prepartition I)

Equations

• BoxIntegral.Prepartition.instOrderTopPrepartitionInstLEPrepartition = OrderTop.mk ⋯

instance BoxIntegral.Prepartition.instOrderBotPrepartitionInstLEPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : OrderBot (BoxIntegral.Prepartition I)

Equations

• BoxIntegral.Prepartition.instOrderBotPrepartitionInstLEPrepartition = OrderBot.mk ⋯

instance BoxIntegral.Prepartition.instInhabitedPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : Inhabited (BoxIntegral.Prepartition I)

Equations

• BoxIntegral.Prepartition.instInhabitedPrepartition = { default := ⊤ }

theorem BoxIntegral.Prepartition.le_def {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} : π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∃ J' ∈ π₂, J ≤ J'

@[simp]

theorem BoxIntegral.Prepartition.mem_top {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : J ∈ ⊤ ↔ J = I

@[simp]

theorem BoxIntegral.Prepartition.top_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} : ⊤.boxes = {I}

@[simp]

theorem BoxIntegral.Prepartition.not_mem_bot {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : J ∉ ⊥

@[simp]

theorem BoxIntegral.Prepartition.bot_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} : ⊥.boxes = ∅

theorem BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (x : ι → ℝ) : Set.InjOn (fun (J : BoxIntegral.Box ι) => {i : ι | J.lower i = x i}) {J : BoxIntegral.Box ι | J ∈ π ∧ x ∈ BoxIntegral.Box.Icc J}

An auxiliary lemma used to prove that the same point can't belong to more than 2 ^ Fintype.card ι closed boxes of a prepartition.

theorem BoxIntegral.Prepartition.card_filter_mem_Icc_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] (x : ι → ℝ) : (Finset.filter (fun (J : BoxIntegral.Box ι) => x ∈ BoxIntegral.Box.Icc J) π.boxes).card ≤ 2 ^ Fintype.card ι

The set of boxes of a prepartition that contain x in their closures has cardinality at most 2 ^ Fintype.card ι.

def BoxIntegral.Prepartition.iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : Set (ι → ℝ)

Given a prepartition π : BoxIntegral.Prepartition I, π.iUnion is the part of I covered by the boxes of π.

Equations

• BoxIntegral.Prepartition.iUnion π = ⋃ J ∈ π, ↑J

theorem BoxIntegral.Prepartition.iUnion_def {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion π = ⋃ J ∈ π, ↑J

theorem BoxIntegral.Prepartition.iUnion_def' {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion π = ⋃ J ∈ π.boxes, ↑J

@[simp]

theorem BoxIntegral.Prepartition.mem_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι → ℝ} : x ∈ BoxIntegral.Prepartition.iUnion π ↔ ∃ J ∈ π, x ∈ J

@[simp]

theorem BoxIntegral.Prepartition.iUnion_single {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (h : J ≤ I) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.single I J h) = ↑J

@[simp]

theorem BoxIntegral.Prepartition.iUnion_top {ι : Type u_1} {I : BoxIntegral.Box ι} : BoxIntegral.Prepartition.iUnion ⊤ = ↑I

@[simp]

theorem BoxIntegral.Prepartition.iUnion_eq_empty {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} : BoxIntegral.Prepartition.iUnion π₁ = ∅ ↔ π₁ = ⊥

@[simp]

theorem BoxIntegral.Prepartition.iUnion_bot {ι : Type u_1} {I : BoxIntegral.Box ι} : BoxIntegral.Prepartition.iUnion ⊥ = ∅

theorem BoxIntegral.Prepartition.subset_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h : J ∈ π) : ↑J ⊆ BoxIntegral.Prepartition.iUnion π

theorem BoxIntegral.Prepartition.iUnion_subset {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion π ⊆ ↑I

theorem BoxIntegral.Prepartition.iUnion_mono {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : π₁ ≤ π₂) : BoxIntegral.Prepartition.iUnion π₁ ⊆ BoxIntegral.Prepartition.iUnion π₂

theorem BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_iUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : Disjoint π₁.boxes π₂.boxes

theorem BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} : π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧ BoxIntegral.Prepartition.iUnion π₁ ⊆ BoxIntegral.Prepartition.iUnion π₂

theorem BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h₁ : π₁.boxes ⊆ π₂.boxes) (h₂ : BoxIntegral.Prepartition.iUnion π₂ ⊆ BoxIntegral.Prepartition.iUnion π₁) : π₁ = π₂

@[simp]

theorem BoxIntegral.Prepartition.biUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : (BoxIntegral.Prepartition.biUnion π πi).boxes = Finset.biUnion π.boxes fun (J : BoxIntegral.Box ι) => (πi J).boxes

def BoxIntegral.Prepartition.biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.Prepartition I

Given a prepartition π of a box I and a collection of prepartitions πi J of all boxes J ∈ π, returns the prepartition of I into the union of the boxes of all πi J.

Though we only use the values of πi on the boxes of π, we require πi to be a globally defined function.

Equations

• BoxIntegral.Prepartition.biUnion π πi = { boxes := Finset.biUnion π.boxes fun (J : BoxIntegral.Box ι) => (πi J).boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[simp]

theorem BoxIntegral.Prepartition.mem_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} : J ∈ BoxIntegral.Prepartition.biUnion π πi ↔ ∃ J' ∈ π, J ∈ πi J'

theorem BoxIntegral.Prepartition.biUnion_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.Prepartition.biUnion π πi ≤ π

@[simp]

theorem BoxIntegral.Prepartition.biUnion_top {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : (BoxIntegral.Prepartition.biUnion π fun (x : BoxIntegral.Box ι) => ⊤) = π

theorem BoxIntegral.Prepartition.biUnion_congr {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} {πi₁ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {πi₂ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : π₁ = π₂) (hi : ∀ J ∈ π₁, πi₁ J = πi₂ J) : BoxIntegral.Prepartition.biUnion π₁ πi₁ = BoxIntegral.Prepartition.biUnion π₂ πi₂

theorem BoxIntegral.Prepartition.biUnion_congr_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} {πi₁ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {πi₂ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : π₁ = π₂) (hi : ∀ J ≤ I, πi₁ J = πi₂ J) : BoxIntegral.Prepartition.biUnion π₁ πi₁ = BoxIntegral.Prepartition.biUnion π₂ πi₂

@[simp]

theorem BoxIntegral.Prepartition.iUnion_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.biUnion π πi) = ⋃ J ∈ π, BoxIntegral.Prepartition.iUnion (πi J)

@[simp]

theorem BoxIntegral.Prepartition.sum_biUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {M : Type u_2} [AddCommMonoid M] (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (f : BoxIntegral.Box ι → M) : (Finset.sum (Finset.biUnion π.boxes fun (J : BoxIntegral.Box ι) => (πi J).boxes) fun (J : BoxIntegral.Box ι) => f J) = Finset.sum π.boxes fun (J : BoxIntegral.Box ι) => Finset.sum (πi J).boxes fun (J' : BoxIntegral.Box ι) => f J'

def BoxIntegral.Prepartition.biUnionIndex {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (J : BoxIntegral.Box ι) : BoxIntegral.Box ι

Given a box J ∈ π.biUnion πi, returns the box J' ∈ π such that J ∈ πi J'. For J ∉ π.biUnion πi, returns I.

Equations

• BoxIntegral.Prepartition.biUnionIndex π πi J = if hJ : J ∈ BoxIntegral.Prepartition.biUnion π πi then Exists.choose ⋯ else I

theorem BoxIntegral.Prepartition.biUnionIndex_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hJ : J ∈ BoxIntegral.Prepartition.biUnion π πi) : BoxIntegral.Prepartition.biUnionIndex π πi J ∈ π

theorem BoxIntegral.Prepartition.biUnionIndex_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (J : BoxIntegral.Box ι) : BoxIntegral.Prepartition.biUnionIndex π πi J ≤ I

theorem BoxIntegral.Prepartition.mem_biUnionIndex {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hJ : J ∈ BoxIntegral.Prepartition.biUnion π πi) : J ∈ πi (BoxIntegral.Prepartition.biUnionIndex π πi J)

theorem BoxIntegral.Prepartition.le_biUnionIndex {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hJ : J ∈ BoxIntegral.Prepartition.biUnion π πi) : J ≤ BoxIntegral.Prepartition.biUnionIndex π πi J

theorem BoxIntegral.Prepartition.biUnionIndex_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (hJ : J ∈ π) {J' : BoxIntegral.Box ι} (hJ' : J' ∈ πi J) : BoxIntegral.Prepartition.biUnionIndex π πi J' = J

Uniqueness property of BoxIntegral.Prepartition.biUnionIndex.

theorem BoxIntegral.Prepartition.biUnion_assoc {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (πi' : BoxIntegral.Box ι → (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : (BoxIntegral.Prepartition.biUnion π fun (J : BoxIntegral.Box ι) => BoxIntegral.Prepartition.biUnion (πi J) (πi' J)) = BoxIntegral.Prepartition.biUnion (BoxIntegral.Prepartition.biUnion π πi) fun (J : BoxIntegral.Box ι) => πi' (BoxIntegral.Prepartition.biUnionIndex π πi J) J

def BoxIntegral.Prepartition.ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint) : BoxIntegral.Prepartition I

Create a BoxIntegral.Prepartition from a collection of possibly empty boxes by filtering out the empty one if it exists.

Equations

• BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint = { boxes := Finset.eraseNone boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[simp]

theorem BoxIntegral.Prepartition.mem_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {boxes : Finset (WithBot (BoxIntegral.Box ι))} {h₁ : ∀ J ∈ boxes, J ≤ ↑I} {h₂ : Set.Pairwise (↑boxes) Disjoint} : J ∈ BoxIntegral.Prepartition.ofWithBot boxes h₁ h₂ ↔ ↑J ∈ boxes

@[simp]

theorem BoxIntegral.Prepartition.iUnion_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint) = ⋃ J ∈ boxes, ↑J

theorem BoxIntegral.Prepartition.ofWithBot_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {boxes : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem : ∀ J ∈ boxes, J ≤ ↑I} {pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint} (H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J') : BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint ≤ π

theorem BoxIntegral.Prepartition.le_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {boxes : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem : ∀ J ∈ boxes, J ≤ ↑I} {pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint} (H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J') : π ≤ BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint

theorem BoxIntegral.Prepartition.ofWithBot_mono {ι : Type u_1} {I : BoxIntegral.Box ι} {boxes₁ : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem₁ : ∀ J ∈ boxes₁, J ≤ ↑I} {pairwise_disjoint₁ : Set.Pairwise (↑boxes₁) Disjoint} {boxes₂ : Finset (WithBot (BoxIntegral.Box ι))} {le_of_mem₂ : ∀ J ∈ boxes₂, J ≤ ↑I} {pairwise_disjoint₂ : Set.Pairwise (↑boxes₂) Disjoint} (H : ∀ J ∈ boxes₁, J ≠ ⊥ → ∃ J' ∈ boxes₂, J ≤ J') : BoxIntegral.Prepartition.ofWithBot boxes₁ le_of_mem₁ pairwise_disjoint₁ ≤ BoxIntegral.Prepartition.ofWithBot boxes₂ le_of_mem₂ pairwise_disjoint₂

theorem BoxIntegral.Prepartition.sum_ofWithBot {ι : Type u_1} {I : BoxIntegral.Box ι} {M : Type u_2} [AddCommMonoid M] (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint) (f : BoxIntegral.Box ι → M) : (Finset.sum (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).boxes fun (J : BoxIntegral.Box ι) => f J) = Finset.sum boxes fun (J : WithBot (BoxIntegral.Box ι)) => Option.elim' 0 f J

def BoxIntegral.Prepartition.restrict {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (J : BoxIntegral.Box ι) : BoxIntegral.Prepartition J

Restrict a prepartition to a box.

Equations

• BoxIntegral.Prepartition.restrict π J = BoxIntegral.Prepartition.ofWithBot (Finset.image (fun (J' : BoxIntegral.Box ι) => ↑J ⊓ ↑J') π.boxes) ⋯ ⋯

@[simp]

theorem BoxIntegral.Prepartition.mem_restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : J₁ ∈ BoxIntegral.Prepartition.restrict π J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ⊓ ↑J'

theorem BoxIntegral.Prepartition.mem_restrict' {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {J₁ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : J₁ ∈ BoxIntegral.Prepartition.restrict π J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ∩ ↑J'

theorem BoxIntegral.Prepartition.restrict_mono {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (Hle : π₁ ≤ π₂) : BoxIntegral.Prepartition.restrict π₁ J ≤ BoxIntegral.Prepartition.restrict π₂ J

theorem BoxIntegral.Prepartition.monotone_restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} : Monotone fun (π : BoxIntegral.Prepartition I) => BoxIntegral.Prepartition.restrict π J

theorem BoxIntegral.Prepartition.restrict_boxes_of_le {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (h : I ≤ J) : (BoxIntegral.Prepartition.restrict π J).boxes = π.boxes

Restricting to a larger box does not change the set of boxes. We cannot claim equality of prepartitions because they have different types.

@[simp]

theorem BoxIntegral.Prepartition.restrict_self {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.restrict π I = π

@[simp]

theorem BoxIntegral.Prepartition.iUnion_restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.restrict π J) = ↑J ∩ BoxIntegral.Prepartition.iUnion π

@[simp]

theorem BoxIntegral.Prepartition.restrict_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (hJ : J ∈ π) : BoxIntegral.Prepartition.restrict (BoxIntegral.Prepartition.biUnion π πi) J = πi J

theorem BoxIntegral.Prepartition.biUnion_le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {π' : BoxIntegral.Prepartition I} : BoxIntegral.Prepartition.biUnion π πi ≤ π' ↔ ∀ J ∈ π, πi J ≤ BoxIntegral.Prepartition.restrict π' J

theorem BoxIntegral.Prepartition.le_biUnion_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} {π' : BoxIntegral.Prepartition I} : π' ≤ BoxIntegral.Prepartition.biUnion π πi ↔ π' ≤ π ∧ ∀ J ∈ π, BoxIntegral.Prepartition.restrict π' J ≤ πi J

instance BoxIntegral.Prepartition.inf {ι : Type u_1} {I : BoxIntegral.Box ι} : Inf (BoxIntegral.Prepartition I)

Equations

• One or more equations did not get rendered due to their size.

theorem BoxIntegral.Prepartition.inf_def {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) : π₁ ⊓ π₂ = BoxIntegral.Prepartition.biUnion π₁ fun (J : BoxIntegral.Box ι) => BoxIntegral.Prepartition.restrict π₂ J

@[simp]

theorem BoxIntegral.Prepartition.mem_inf {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} : J ∈ π₁ ⊓ π₂ ↔ ∃ J₁ ∈ π₁, ∃ J₂ ∈ π₂, ↑J = ↑J₁ ⊓ ↑J₂

@[simp]

theorem BoxIntegral.Prepartition.iUnion_inf {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion (π₁ ⊓ π₂) = BoxIntegral.Prepartition.iUnion π₁ ∩ BoxIntegral.Prepartition.iUnion π₂

instance BoxIntegral.Prepartition.instSemilatticeInfPrepartition {ι : Type u_1} {I : BoxIntegral.Box ι} : SemilatticeInf (BoxIntegral.Prepartition I)

Equations

• BoxIntegral.Prepartition.instSemilatticeInfPrepartition = let __src := BoxIntegral.Prepartition.inf; let __src_1 := BoxIntegral.Prepartition.partialOrder; SemilatticeInf.mk ⋯ ⋯ ⋯

@[simp]

theorem BoxIntegral.Prepartition.filter_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : (BoxIntegral.Prepartition.filter π p).boxes = Finset.filter p π.boxes

def BoxIntegral.Prepartition.filter {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : BoxIntegral.Prepartition I

The prepartition with boxes {J ∈ π | p J}.

Equations

• BoxIntegral.Prepartition.filter π p = { boxes := Finset.filter p π.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[simp]

theorem BoxIntegral.Prepartition.mem_filter {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {p : BoxIntegral.Box ι → Prop} : J ∈ BoxIntegral.Prepartition.filter π p ↔ J ∈ π ∧ p J

theorem BoxIntegral.Prepartition.filter_le {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : BoxIntegral.Prepartition.filter π p ≤ π

theorem BoxIntegral.Prepartition.filter_of_true {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {p : BoxIntegral.Box ι → Prop} (hp : ∀ J ∈ π, p J) : BoxIntegral.Prepartition.filter π p = π

@[simp]

theorem BoxIntegral.Prepartition.filter_true {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : (BoxIntegral.Prepartition.filter π fun (x : BoxIntegral.Box ι) => True) = π

@[simp]

theorem BoxIntegral.Prepartition.iUnion_filter_not {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.filter π fun (J : BoxIntegral.Box ι) => ¬p J) = BoxIntegral.Prepartition.iUnion π \ BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.filter π p)

theorem BoxIntegral.Prepartition.sum_fiberwise {ι : Type u_1} {I : BoxIntegral.Box ι} {α : Type u_2} {M : Type u_3} [AddCommMonoid M] (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → α) (g : BoxIntegral.Box ι → M) : (Finset.sum (Finset.image f π.boxes) fun (y : α) => Finset.sum (BoxIntegral.Prepartition.filter π fun (J : BoxIntegral.Box ι) => f J = y).boxes fun (J : BoxIntegral.Box ι) => g J) = Finset.sum π.boxes fun (J : BoxIntegral.Box ι) => g J

@[simp]

theorem BoxIntegral.Prepartition.disjUnion_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : (BoxIntegral.Prepartition.disjUnion π₁ π₂ h).boxes = π₁.boxes ∪ π₂.boxes

def BoxIntegral.Prepartition.disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.Prepartition I) (π₂ : BoxIntegral.Prepartition I) (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : BoxIntegral.Prepartition I

Union of two disjoint prepartitions.

Equations

• BoxIntegral.Prepartition.disjUnion π₁ π₂ h = { boxes := π₁.boxes ∪ π₂.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }

@[simp]

theorem BoxIntegral.Prepartition.mem_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (H : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : J ∈ BoxIntegral.Prepartition.disjUnion π₁ π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

@[simp]

theorem BoxIntegral.Prepartition.iUnion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.disjUnion π₁ π₂ h) = BoxIntegral.Prepartition.iUnion π₁ ∪ BoxIntegral.Prepartition.iUnion π₂

@[simp]

theorem BoxIntegral.Prepartition.sum_disj_union_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} {M : Type u_2} [AddCommMonoid M] (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) (f : BoxIntegral.Box ι → M) : (Finset.sum (π₁.boxes ∪ π₂.boxes) fun (J : BoxIntegral.Box ι) => f J) = (Finset.sum π₁.boxes fun (J : BoxIntegral.Box ι) => f J) + Finset.sum π₂.boxes fun (J : BoxIntegral.Box ι) => f J

def BoxIntegral.Prepartition.distortion {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] : NNReal

The distortion of a prepartition is the maximum of the distortions of the boxes of this prepartition.

Equations

• BoxIntegral.Prepartition.distortion π = Finset.sup π.boxes BoxIntegral.Box.distortion

theorem BoxIntegral.Prepartition.distortion_le_of_mem {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] (h : J ∈ π) : BoxIntegral.Box.distortion J ≤ BoxIntegral.Prepartition.distortion π

theorem BoxIntegral.Prepartition.distortion_le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] {c : NNReal} : BoxIntegral.Prepartition.distortion π ≤ c ↔ ∀ J ∈ π, BoxIntegral.Box.distortion J ≤ c

theorem BoxIntegral.Prepartition.distortion_biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} [Fintype ι] (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) : BoxIntegral.Prepartition.distortion (BoxIntegral.Prepartition.biUnion π πi) = Finset.sup π.boxes fun (J : BoxIntegral.Box ι) => BoxIntegral.Prepartition.distortion (πi J)

@[simp]

theorem BoxIntegral.Prepartition.distortion_disjUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} [Fintype ι] (h : Disjoint (BoxIntegral.Prepartition.iUnion π₁) (BoxIntegral.Prepartition.iUnion π₂)) : BoxIntegral.Prepartition.distortion (BoxIntegral.Prepartition.disjUnion π₁ π₂ h) = max (BoxIntegral.Prepartition.distortion π₁) (BoxIntegral.Prepartition.distortion π₂)

theorem BoxIntegral.Prepartition.distortion_of_const {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [Fintype ι] {c : NNReal} (h₁ : π.boxes.Nonempty) (h₂ : ∀ J ∈ π, BoxIntegral.Box.distortion J = c) : BoxIntegral.Prepartition.distortion π = c

@[simp]

theorem BoxIntegral.Prepartition.distortion_top {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : BoxIntegral.Prepartition.distortion ⊤ = BoxIntegral.Box.distortion I

@[simp]

theorem BoxIntegral.Prepartition.distortion_bot {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) : BoxIntegral.Prepartition.distortion ⊥ = 0

def BoxIntegral.Prepartition.IsPartition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) : Prop

A prepartition π of I is a partition if the boxes of π cover the whole I.

Equations

• BoxIntegral.Prepartition.IsPartition π = ∀ x ∈ I, ∃ J ∈ π, x ∈ J

theorem BoxIntegral.Prepartition.isPartition_iff_iUnion_eq {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} : BoxIntegral.Prepartition.IsPartition π ↔ BoxIntegral.Prepartition.iUnion π = ↑I

@[simp]

theorem BoxIntegral.Prepartition.isPartition_single_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (h : J ≤ I) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.single I J h) ↔ J = I

theorem BoxIntegral.Prepartition.isPartitionTop {ι : Type u_1} (I : BoxIntegral.Box ι) : BoxIntegral.Prepartition.IsPartition ⊤

theorem BoxIntegral.Prepartition.IsPartition.iUnion_eq {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) : BoxIntegral.Prepartition.iUnion π = ↑I

theorem BoxIntegral.Prepartition.IsPartition.iUnion_subset {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) (π₁ : BoxIntegral.Prepartition I) : BoxIntegral.Prepartition.iUnion π₁ ⊆ BoxIntegral.Prepartition.iUnion π

theorem BoxIntegral.Prepartition.IsPartition.existsUnique {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {x : ι → ℝ} (h : BoxIntegral.Prepartition.IsPartition π) (hx : x ∈ I) : ∃! (J : BoxIntegral.Box ι), ∃! (x_1 : J ∈ π), x ∈ J

theorem BoxIntegral.Prepartition.IsPartition.nonempty_boxes {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) : π.boxes.Nonempty

theorem BoxIntegral.Prepartition.IsPartition.eq_of_boxes_subset {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h₁ : BoxIntegral.Prepartition.IsPartition π₁) (h₂ : π₁.boxes ⊆ π₂.boxes) : π₁ = π₂

theorem BoxIntegral.Prepartition.IsPartition.le_iff {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π₂) : π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∀ J' ∈ π₂, Set.Nonempty (↑J ∩ ↑J') → J ≤ J'

theorem BoxIntegral.Prepartition.IsPartition.biUnion {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : BoxIntegral.Prepartition.IsPartition π) (hi : ∀ J ∈ π, BoxIntegral.Prepartition.IsPartition (πi J)) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.biUnion π πi)

theorem BoxIntegral.Prepartition.IsPartition.restrict {ι : Type u_1} {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) (hJ : J ≤ I) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.restrict π J)

theorem BoxIntegral.Prepartition.IsPartition.inf {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h₁ : BoxIntegral.Prepartition.IsPartition π₁) (h₂ : BoxIntegral.Prepartition.IsPartition π₂) : BoxIntegral.Prepartition.IsPartition (π₁ ⊓ π₂)

theorem BoxIntegral.Prepartition.iUnion_biUnion_partition {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J} (h : ∀ J ∈ π, BoxIntegral.Prepartition.IsPartition (πi J)) : BoxIntegral.Prepartition.iUnion (BoxIntegral.Prepartition.biUnion π πi) = BoxIntegral.Prepartition.iUnion π

theorem BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.iUnion π₂ = ↑I \ BoxIntegral.Prepartition.iUnion π₁) : BoxIntegral.Prepartition.IsPartition (BoxIntegral.Prepartition.disjUnion π₁ π₂ ⋯)