Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.variation_map_le

∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {Y : Type u_3} [inst_3 : MeasurableSpace Y] {φ : X → Y},
  (μ.map φ).variation ≤ MeasureTheory.Measure.map φ μ.variation

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites20

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
AddCommMonoidproof · cited by 12,281
MeasureTheory.Measurestatement and proof · cited by 10,939
Set.preimageproof · cited by 4,946
MeasurableSetproof · cited by 3,075
Measurableproof · cited by 1,499
T2Spacestatement and proof · cited by 1,351
MeasureTheory.Measure.mapstatement and proof · cited by 858
ENorm.enormproof · cited by 715
MeasureTheory.VectorMeasurestatement and proof · cited by 451

Cited by4

Results whose statement or proof uses this declaration.

MeasurableEmbedding.variation_mapproof · cited by 3
MeasureTheory.VectorMeasure.integral_mapproof · cited by 2
MeasureTheory.VectorMeasure.Integrable.mapproof · cited by 0
MeasureTheory.VectorMeasure.variation_transpose_map_leproof · cited by 0