Theorems · Theorem · measure theory

MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub.congr_simp

∀ {X : Type u_1} {mX : MeasurableSpace X} (μ μ_1 : MeasureTheory.Measure X) (e_μ : μ = μ_1)
  (ν ν_1 : MeasureTheory.Measure X) (e_ν : ν = ν_1) [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  μ.jordanDecompositionOfToSignedMeasureSub ν = μ_1.jordanDecompositionOfToSignedMeasureSub ν_1

Defined in: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Cited by: 0 results in Mathlib
Foundations: Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.IsFiniteMeasure MeasureTheory.IsFiniteMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
MeasureTheory.JordanDecompositionstatement · cited by 40
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSubstatement and proof · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.