Theorems · Theorem · measure theory

MeasureTheory.charFunDual_eq_charFun_map_one

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} [OpensMeasurableSpace E] (L : StrongDual ℝ E),
  MeasureTheory.charFunDual μ L = MeasureTheory.charFun (MeasureTheory.Measure.map (⇑L) μ) 1

Defined in

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceOpensMeasurableSpace