Theorems · Theorem · measure theory

ae_restrict_iff_subtype

∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ {p : α → Prop}, (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : ↑s) ∂MeasureTheory.Measure.comap Subtype.val μ, p ↑x

Defined in: Mathlib.MeasureTheory.Measure.Restrict
Cited by: 1 results in Mathlib
Foundations: Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound

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
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Set.Elemstatement and proof · cited by 7,166
Filter.Eventuallystatement and proof · cited by 3,134
MeasurableSetstatement and proof · cited by 3,075
MeasureTheory.aestatement and proof · cited by 2,352
MeasureTheory.Measure.restrictstatement · cited by 1,646
MeasureTheory.Measure.comapstatement and proof · cited by 96
MeasurableEmbedding.subtype_coeproof · cited by 27
map_comap_subtype_coeproof · cited by 14
MeasurableEmbedding.ae_map_iffproof · cited by 6

Cited by1

Results whose statement or proof uses this declaration.

IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero'proof · cited by 1