Theorems · Theorem · number theory

AbstractMeasure.contractSnd_apply

∀ {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 Y R R)
  (f : C(X × Y, R)) (x : X),
  ((AbstractMeasure.contractSnd ν) f) x = ν { toFun := fun y => f (x, y), continuous_toFun := ⋯ }

Defined in

Mathlib.NumberTheory.Padics.Measure.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceCommRingTopologicalSpaceIsTopologicalRing