ι : Type u_1
M : Type ?u.55340
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ splitMany I s ≤ π
ι : Type u_1
M : Type ?u.55340
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
⊢ ∃ s, splitMany I s ≤ π
refine' (eventually_splitMany_inf_eq_filter π).exists.imp fun s hs => _
case hp
ι : Type u_1
M : Type ?u.55340
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ ↑I
⊢ ∀ (J : Box ι), J ∈ splitMany I s → ↑J ⊆ ↑I
ι : Type u_1
M : Type ?u.55340
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ splitMany I s ≤ π
rwa [h.iUnion_eq, filter_of_true, inf_eq_right] at hs
no goals
case hp
ι : Type u_1
M : Type ?u.55340
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ ↑I
⊢ ∀ (J : Box ι), J ∈ splitMany I s → ↑J ⊆ ↑I
exact fun J hJ => le_of_mem _ hJ