Theorems · Theorem · measure theory

MeasureTheory.Measure.sigmaFiniteSetGE.congr_simp

∀ {α : Type u_1} {mα : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α),
  μ = μ_1 →
    ∀ (ν ν_1 : MeasureTheory.Measure α) (e_ν : ν = ν_1) [inst : MeasureTheory.IsFiniteMeasure ν] (n n_1 : ℕ),
      n = n_1 → ∀ (a a_1 : α), a = a_1 → μ.sigmaFiniteSetGE ν n a = μ_1.sigmaFiniteSetGE ν_1 n_1 a_1

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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.Measure.sigmaFiniteSetGEstatement and proof · cited by 8

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.