case intro
ι : Type u_1
M : Type ?u.56100
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π
ι : Type u_1
M : Type ?u.56100
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
⊢ ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π
rcases π.eventually_splitMany_inf_eq_filter.exists with ⟨s, hs⟩
case intro
ι : Type u_1
M : Type ?u.56100
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ Prepartition.iUnion (filter (splitMany I s) fun J => ¬↑J ⊆ Prepartition.iUnion π) = ↑I \ Prepartition.iUnion π
case intro
ι : Type u_1
M : Type ?u.56100
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π
use (splitMany I s).filter fun J => ¬(J : Set (ι → ℝ)) ⊆ π.iUnion
no goals
case intro
ι : Type u_1
M : Type ?u.56100
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ Prepartition.iUnion (filter (splitMany I s) fun J => ¬↑J ⊆ Prepartition.iUnion π) = ↑I \ Prepartition.iUnion π
simp [← hs]