Theorems · Theorem · measure theory

MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite

∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
  [inst_1 : TopologicalSpace β] [T2Space β],
  MeasureTheory.FinStronglyMeasurable f μ →
    ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ MeasureTheory.SigmaFinite (μ.restrict t)

Defined in: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Cited by: 3 results in Mathlib
Foundations: Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Zero TopologicalSpace T2Space

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites35

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

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealproof · cited by 9,879
Top.topproof · cited by 9,680
nhdsproof · cited by 5,554
Set.univproof · cited by 3,945
Filter.Tendstoproof · cited by 3,814
MeasurableSetstatement and proof · cited by 3,075
Compl.complstatement and proof · cited by 2,925

Cited by3

Results whose statement or proof uses this declaration.

MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFiniteproof · cited by 3
MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trimproof · cited by 1
MeasureTheory.finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFiniteproof · cited by 0