case empty
ι : Type u_1
M : Type ?u.45780
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
⊢ π ⊓ splitMany I ∅ = biUnion π fun J => splitMany J ∅

case insert
ι : Type u_1
M : Type ?u.45780
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬p ∈ s
ihp : π ⊓ splitMany I s = biUnion π fun J => splitMany J s
⊢ π ⊓ splitMany I (insert p s) = biUnion π fun J => splitMany J (insert p s)
ι : Type u_1
M : Type ?u.45780
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
⊢ π ⊓ splitMany I s = biUnion π fun J => splitMany J s
induction' s using Finset.induction_on with p s _ ihp
no goals
case empty
ι : Type u_1
M : Type ?u.45780
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
⊢ π ⊓ splitMany I ∅ = biUnion π fun J => splitMany J ∅
simp
no goals
case insert
ι : Type u_1
M : Type ?u.45780
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬p ∈ s
ihp : π ⊓ splitMany I s = biUnion π fun J => splitMany J s
⊢ π ⊓ splitMany I (insert p s) = biUnion π fun J => splitMany J (insert p s)
simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]