Theorems · Theorem · real analysis

BoxIntegral.Prepartition.iUnion_biUnion_partition

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
  (∀ J ∈ π, (πi J).IsPartition) → (π.biUnion πi).iUnion = π.iUnion

Defined in: Mathlib.Analysis.BoxIntegral.Partition.Basic
Cited by: 3 results in Mathlib
Foundations: Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

Setstatement · cited by 53,352
Realstatement · cited by 25,697
BoxIntegral.Boxstatement and proof · cited by 464
BoxIntegral.Prepartitionstatement and proof · cited by 199
BoxIntegral.Prepartition.iUnionstatement · cited by 71
BoxIntegral.Prepartition.IsPartitionstatement and proof · cited by 30
BoxIntegral.Prepartition.biUnionstatement · cited by 24
BoxIntegral.Prepartition.IsPartition.iUnion_eqproof · cited by 9
Set.iUnion_congr_of_surjectiveproof · cited by 6
BoxIntegral.Prepartition.iUnion_biUnionproof · cited by 4

Cited by3

Results whose statement or proof uses this declaration.

BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eqproof · cited by 6
BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eqproof · cited by 2
BoxIntegral.IntegrationParams.biUnionTagged_memBaseSetproof · cited by 1