Theorems · Theorem · real analysis

BoxIntegral.Prepartition.forall_biUnionTagged

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (p : (ι → ℝ) → BoxIntegral.Box ι → Prop) (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J),
  (∀ J ∈ π.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Tagged

Cited by

2 results in Mathlib

Foundations

Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound