Theorems · Definition · real analysis

BoxIntegral.TaggedPrepartition.IsSubordinate

{ι : Type u_1} →
  {I : BoxIntegral.Box ι} → [Fintype ι] → BoxIntegral.TaggedPrepartition I → ((ι → ℝ) → ↑(Set.Ioi 0)) → Prop

A tagged partition π is subordinate to r : (ι → ℝ) → ℝ if each box J ∈ π is included in the closed ball with center π.tag J and radius r (π.tag J).

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Tagged

Cited by

15 results in Mathlib

Foundations

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

Assumes

Fintype