Theorems · Definition · real analysis

BoxIntegral.IntegrationParams.toFilter

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

A set s : Set (TaggedPrepartition I) belongs to l.toFilter I if for any c : ℝ≥0 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 π.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Filter

Cited by

5 results in Mathlib

Foundations

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

Assumes

Fintype