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 ι
⊢ HasBasis (toFilteriUnion l I ⊤) (fun r => ∀ (c : ℝ≥0), RCond l (r c)) fun r =>
    {π | ∃ c, MemBaseSet l I c (r c) π ∧ IsPartition π}
simpa only [TaggedPrepartition.isPartition_iff_iUnion_eq, Prepartition.iUnion_top] using
  l.hasBasis_toFilteriUnion I ⊤