ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Box.distortion I ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
rw [← Prepartition.distortion_top] at hc
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
hc' : Prepartition.distortion (Prepartition.compl ⊤) ≤ c
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
have hc' : (⊤ : Prepartition I).compl.distortion ≤ c := by simp
no goals
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
hc' : Prepartition.distortion (Prepartition.compl ⊤) ≤ c
⊢ ∃ π, MemBaseSet l I c r π ∧ IsPartition π
simpa [isPartition_iff_iUnion_eq] using l.exists_memBaseSet_le_iUnion_eq ⊤ hc hc' r
no goals
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
c c₁ c₂ : ℝ≥0
r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π π₁ π₂ : TaggedPrepartition I✝
l✝ l₁ l₂ l : IntegrationParams
I : Box ι
hc : Prepartition.distortion ⊤ ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ Prepartition.distortion (Prepartition.compl ⊤) ≤ c
simp