Theorems · Theorem · real analysis

BoxIntegral.Prepartition.iUnion_ofWithBot

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι)))
  (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint),
  (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Basic

Cited by

2 results in Mathlib

Foundations

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