Theorems · Definition · real analysis

BoxIntegral.IntegrationParams.toFilterDistortioniUnion

{ι : Type u_1} →
  [Fintype ι] →
    BoxIntegral.IntegrationParams →
      (I : BoxIntegral.Box ι) → NNReal → BoxIntegral.Prepartition I → Filter (BoxIntegral.TaggedPrepartition I)

A set s : Set (TaggedPrepartition I) belongs to l.toFilterDistortioniUnion I c π₀ if there exists a function r : ℝⁿ → (0, ∞) (or a constant r if l.bRiemann = true) such that s contains each prepartition π such that l.MemBaseSet I c r π and π.iUnion = π₀.iUnion.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Filter

Cited by

4 results in Mathlib

Foundations

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

Assumes

Fintype