Theorems · Inductive type · real analysis

BoxIntegral.BoxAdditiveMap

(ι : Type u_3) → (M : Type u_4) → [AddCommMonoid M] → WithTop (BoxIntegral.Box ι) → Type (max u_3 u_4)

A function on Box ι is called box additive if for every box J and a partition π of J we have f J = ∑ Ji ∈ π.boxes, f Ji. A function is called box additive on subboxes of I : Box ι if the same property holds for J ≤ I. We formalize these two notions in the same definition using I : WithBot (Box ι): the value I = ⊤ corresponds to functions box additive on the whole space.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Additive

Cited by

92 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

AddCommMonoid