Theorems · Theorem · real analysis

BoxIntegral.Prepartition.ofWithBot_le

∀ {ι : 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 ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J') → BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint ≤ π

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Basic

Cited by

0 results in Mathlib

Foundations

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