Theorems · Theorem · real analysis

BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [Finite ι] (s : Set (BoxIntegral.Prepartition I)),
  s.Finite →
    ∃ t,
      ∀ π ∈ s,
        π ⊓ BoxIntegral.Prepartition.splitMany I t =
          (BoxIntegral.Prepartition.splitMany I t).filter fun J => ↑J ⊆ π.iUnion

Defined in: Mathlib.Analysis.BoxIntegral.Partition.Split
Cited by: 1 results in Mathlib
Foundations: Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Realstatement · cited by 25,697
Finsetstatement · cited by 13,712
Finitestatement and proof · cited by 3,029
Set.Finitestatement and proof · cited by 1,814
BoxIntegral.Boxstatement and proof · cited by 464
BoxIntegral.Prepartitionstatement and proof · cited by 199
Filter.Eventually.existsproof · cited by 168
BoxIntegral.Box.toSetstatement · cited by 121
BoxIntegral.Prepartition.iUnionstatement · cited by 71
BoxIntegral.Prepartition.filterstatement · cited by 14
BoxIntegral.Prepartition.splitManystatement · cited by 13

Cited by1

Results whose statement or proof uses this declaration.

BoxIntegral.BoxAdditiveMap.sum_boxes_congrproof · cited by 0