Theorems · Definition · real analysis

BoxIntegral.TaggedPrepartition.unionComplToSubordinate

{ι : Type u_1} →
  [Fintype ι] →
    {I : BoxIntegral.Box ι} →
      (π₁ : BoxIntegral.TaggedPrepartition I) →
        (π₂ : BoxIntegral.Prepartition I) →
          π₂.iUnion = ↑I \ π₁.iUnion → ((ι → ℝ) → ↑(Set.Ioi 0)) → BoxIntegral.TaggedPrepartition I

Given a tagged prepartition π₁, a prepartition π₂ that covers exactly I \ π₁.iUnion, and a function r : ℝⁿ → (0, ∞), returns the union of π₁ and π₂.toSubordinate r. This partition π has the following properties: * π is a partition, i.e. it covers the whole I; * π₁.boxes ⊆ π.boxes; * π.tag J = π₁.tag J whenever J ∈ π₁; * π is Henstock outside of π₁: π.tag J ∈ J.Icc whenever J ∈ π, J ∉ π₁; * π is subordinate to r outside of π₁; * the distortion of π is equal to the maximum of the distortions of π₁ and π₂.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Cited by

7 results in Mathlib

Foundations

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

Assumes

Fintype