Theorems · Theorem · measure theory

stronglyMeasurable_of_restrict_of_restrict_compl

∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β} {s : Set α},
  MeasurableSet s →
    MeasureTheory.StronglyMeasurable (s.domRestrict f) →
      MeasureTheory.StronglyMeasurable (sᶜ.domRestrict f) → MeasureTheory.StronglyMeasurable f

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
Set.Elemstatement · cited by 7,166
MeasurableSetstatement and proof · cited by 3,075
Compl.complstatement and proof · cited by 2,925
Set.domRestrictstatement and proof · cited by 383
Eq.geproof · cited by 375
MeasureTheory.StronglyMeasurablestatement and proof · cited by 363
MeasurableSet.complproof · cited by 172
Set.union_compl_selfproof · cited by 57
stronglyMeasurable_of_stronglyMeasurable_union_coverproof · cited by 1

Cited by3

Results whose statement or proof uses this declaration.

MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_onproof · cited by 2
MeasureTheory.StronglyMeasurable.tsumproof · cited by 1
MeasureTheory.StronglyMeasurable.tprodproof · cited by 1