Commit 2024-08-15 09:43 d49e5525

View on Github →

feat: Add IsCaratheodory lemmas (#15265) Add isCaratheodory_diff, isCaratheodory_partialSups and isCaratheodory_disjointed. Generalize isCaratheodory_iUnion_nat.

Estimated changes

Modified Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean

added theorem MeasureTheory.OuterMeasure.isCaratheodory_diff

added theorem MeasureTheory.OuterMeasure.isCaratheodory_disjointed

added theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_nat

added theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint

added theorem MeasureTheory.OuterMeasure.isCaratheodory_partialSups