Theorems · Definition · measure theory
MeasureTheory.OuterMeasure.IsCaratheodory
{α : Type u} → MeasureTheory.OuterMeasure α → Set α → PropA set s is Carathéodory-measurable for an outer measure m if for all sets t we have
m t = m (t ∩ s) + m (t \ s).
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- MeasureTheory.OuterMeasurestatement and proof · cited by 287
Cited by21
Results whose statement or proof uses this declaration.
- MeasureTheory.OuterMeasure.isCaratheodory_complstatement · cited by 4
- MeasureTheory.OuterMeasure.isCaratheodory_iff_le'statement · cited by 3
- MeasureTheory.OuterMeasure.isCaratheodory_sdiffstatement and proof · cited by 2
- MeasureTheory.OuterMeasure.isCaratheodory_sumstatement and proof · cited by 2
- MeasureTheory.OuterMeasure.isCaratheodory_unionstatement and proof · cited by 2
- MeasureTheory.OuterMeasure.isCaratheodory_compl_iffstatement and proof · cited by 1
- MeasureTheory.OuterMeasure.IsCaratheodory.biUnion_of_finitestatement and proof · cited by 1
- MeasureTheory.OuterMeasure.isCaratheodory_disjointedstatement and proof · cited by 1
- MeasureTheory.OuterMeasure.isCaratheodory_emptystatement · cited by 1
- MeasureTheory.OuterMeasure.isCaratheodory_iUnionstatement and proof · cited by 1
- MeasureTheory.OuterMeasure.isCaratheodory_iUnion_ltstatement and proof · cited by 1
- MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjointstatement and proof · cited by 1