Theorems · Theorem · real analysis

BoxIntegral.Prepartition.le_ofWithBot

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {boxes : Finset (WithBot (BoxIntegral.Box ι))}
  {le_of_mem : ∀ J ∈ boxes, J ≤ ↑I} {pairwise_disjoint : (↑boxes).Pairwise Disjoint},
  (∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J') → π ≤ BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Basic

Cited by

1 results in Mathlib

Foundations

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