Theorems · Definition · number theory

AbstractMeasure.contractFst

{X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] → AbstractMeasure X R R →ₗ[R] C(X × Y, R) →ₗ[R] C(Y, R)

Send a measure μ on X and a function f on X × Y to the function on Y given by y ↦ μ (f (·, y)), or more suggestively, y ↦ ∫ f(x, y) dμ(x).

Defined in

Mathlib.NumberTheory.Padics.Measure.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceCommRingTopologicalSpaceIsTopologicalRing