Theorems · Theorem · real analysis

BoxIntegral.unitPartition.prepartition_isSubordinate

∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] (B : BoxIntegral.Box ι) {r : ℝ} (hr : 0 < r),
  1 / ↑n ≤ r → (BoxIntegral.unitPartition.prepartition n B).IsSubordinate fun x => ⟨r, hr⟩

Defined in

Mathlib.Analysis.BoxIntegral.UnitPartition

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZeroFintype