Theorems · Theorem · real analysis

BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate

∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I)
  (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
  (π₁.unionComplToSubordinate π₂ hU r).IsPartition

Defined in: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
Cited by: 2 results in Mathlib
Foundations: Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites15

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

Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
Fintypestatement and proof · cited by 7,736
Set.Elemstatement and proof · cited by 7,166
Set.Ioistatement and proof · cited by 1,463
BoxIntegral.Boxstatement and proof · cited by 464
BoxIntegral.Prepartitionstatement and proof · cited by 199
BoxIntegral.TaggedPrepartitionstatement and proof · cited by 126
BoxIntegral.Box.toSetstatement and proof · cited by 121
BoxIntegral.Prepartition.iUnionstatement and proof · cited by 71
BoxIntegral.TaggedPrepartition.iUnionstatement and proof · cited by 51
BoxIntegral.TaggedPrepartition.IsPartitionstatement · cited by 27

Cited by2

Results whose statement or proof uses this declaration.

BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSetproof · cited by 2
BoxIntegral.TaggedPrepartition.iUnion_unionComplToSubordinate_boxesproof · cited by 1