no goals
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
⊢ (∀ (ib : ℝ),
      0 < ib →
        ∃ ia,
          (∀ (c : ℝ≥0), RCond l (ia c)) ∧
            ∀ (x : TaggedPrepartition I),
              x ∈ {π | ∃ c, MemBaseSet l I c (ia c) π ∧ IsPartition π} → integralSum f vol x ∈ closedBall y ib) ↔
    ∀ (ε : ℝ),
      ε > 0 →
        ∃ r,
          (∀ (c : ℝ≥0), RCond l (r c)) ∧
            ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
              MemBaseSet l I c (r c) π → IsPartition π → dist (integralSum f vol π) y ≤ ε
simp [@forall_swap ℝ≥0 (TaggedPrepartition I)]