Theorems · Definition · real analysis

BoxIntegral.BoxAdditiveMap.map

{ι : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : AddCommMonoid N] →
          {I₀ : WithTop (BoxIntegral.Box ι)} →
            BoxIntegral.BoxAdditiveMap ι M I₀ → (M →+ N) → BoxIntegral.BoxAdditiveMap ι N I₀

If g : M → N is an additive map and f is a box additive map, then g ∘ f is a box additive map.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Additive

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid