Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.variation_dirac

∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {x : X} {v : V},
  (MeasureTheory.VectorMeasure.dirac x v).variation = ‖v‖ₑ • MeasureTheory.Measure.dirac x

Defined in: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace ENormedAddCommMonoid T2Space

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites25

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setproof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement · cited by 9,879
mul_oneproof · cited by 3,885
MeasurableSetproof · cited by 3,075
MulZeroClass.mul_zeroproof · cited by 2,091
le_antisymmproof · cited by 2,068
T2Spacestatement and proof · cited by 1,351
le_transproof · cited by 985
ENorm.enormstatement and proof · cited by 715

Cited by2

Results whose statement or proof uses this declaration.

MeasureTheory.VectorMeasure.integral_diracproof · cited by 2
MeasureTheory.VectorMeasure.integral_dirac'proof · cited by 2