Caratheodory

📁 Source: Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean

Statistics

Metric	Count
Definitions `IsCaratheodory`, `caratheodory`, `caratheodoryDynkin`	3
Theorems `biUnion_of_finite`, `boundedBy_caratheodory`, `dirac_caratheodory`, `f_iUnion`, `iUnion_eq_of_caratheodory`, `isCaratheodory_compl`, `isCaratheodory_compl_iff`, `isCaratheodory_diff`, `isCaratheodory_disjointed`, `isCaratheodory_empty`, `isCaratheodory_iUnion`, `isCaratheodory_iUnion_lt`, `isCaratheodory_iUnion_of_disjoint`, `isCaratheodory_iff`, `isCaratheodory_iff_le`, `isCaratheodory_iff_le'`, `isCaratheodory_inter`, `isCaratheodory_partialSups`, `isCaratheodory_sum`, `isCaratheodory_union`, `le_add_caratheodory`, `le_smul_caratheodory`, `le_sum_caratheodory`, `measure_inter_union`, `ofFunction_caratheodory`, `top_caratheodory`, `zero_caratheodory`	27
Total	30

MeasureTheory.OuterMeasure

Definitions

Name	Category	Theorems
`IsCaratheodory` 📖	MathDef	6 math math: `MeasureTheory.AddContent.isCaratheodory_ofFunction_of_mem`, `isCaratheodory_iff_le'`, `MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem`, `isCaratheodory_empty`, `MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure`, `isCaratheodory_compl_iff`
`caratheodory` 📖	CompOp	23 math math: `IsMetric.borel_le_caratheodory`, `IsMetric.le_caratheodory`, `boundedBy_caratheodory`, `MeasureTheory.inducedOuterMeasure_caratheodory`, `MeasureTheory.Measure.sInf_caratheodory`, `le_sum_caratheodory`, `isCaratheodory_iff`, `PMF.toOuterMeasure_caratheodory`, `StieltjesFunction.borel_le_measurable`, `le_add_caratheodory`, `StieltjesFunction.measurableSet_Ioi`, `zero_caratheodory`, `top_caratheodory`, `MeasureTheory.Measure.pi_caratheodory`, `isCaratheodory_iff_le`, `le_smul_caratheodory`, `MeasureTheory.Content.outerMeasure_caratheodory`, `MeasureTheory.Content.borel_le_caratheodory`, `MeasureTheory.AddContent.measureCaratheodory_eq_inducedOuterMeasure`, `MeasureTheory.le_toOuterMeasure_caratheodory`, `ofFunction_caratheodory`, `dirac_caratheodory`, `MeasureTheory.AddContent.measureCaratheodory_eq`
`caratheodoryDynkin` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundedBy_caratheodory` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Set` `Set.instInter` `Set.instSDiff`	`MeasurableSet` `caratheodory` `boundedBy`	—	`ofFunction_caratheodory` `Set.eq_empty_or_nonempty` `iSup_congr_Prop` `Set.empty_inter` `iSup_neg` `bot_eq_zero'` `ENNReal.instCanonicallyOrderedAdd` `Set.empty_diff` `add_zero` `iSup_pos` `le_trans` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `iSup_const_le`
`dirac_caratheodory` 📖	mathematical	—	`caratheodory` `dirac` `Top.top` `MeasurableSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`top_unique` `Set.indicator_of_mem` `Set.indicator_of_notMem` `add_zero` `zero_add`
`f_iUnion` 📖	mathematical	`IsCaratheodory` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `ENNReal` `instFunLikeSetENNReal` `Set.iUnion` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	`le_antisymm` `MeasureTheory.measure_iUnion_le` `instOuterMeasureClass` `instCountableNat` `ENNReal.tsum_eq_iSup_nat` `iSup_le` `isCaratheodory_sum` `Finset.sum_congr` `Set.inter_comm` `Set.inter_univ` `Set.univ_inter` `mono` `Set.iUnion₂_subset` `Set.subset_iUnion`
`iUnion_eq_of_caratheodory` 📖	mathematical	`MeasurableSet` `caratheodory` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `ENNReal` `instFunLikeSetENNReal` `Set.iUnion` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	`f_iUnion`
`isCaratheodory_compl` 📖	mathematical	`IsCaratheodory`	`Compl.compl` `Set` `Set.instCompl`	—	`Set.inter_comm` `sdiff_compl` `add_comm`
`isCaratheodory_compl_iff` 📖	mathematical	—	`IsCaratheodory` `Compl.compl` `Set` `Set.instCompl`	—	`compl_compl` `isCaratheodory_compl`
`isCaratheodory_diff` 📖	mathematical	`IsCaratheodory`	`Set` `Set.instSDiff`	—	`isCaratheodory_inter` `isCaratheodory_compl`
`isCaratheodory_disjointed` 📖	mathematical	`IsCaratheodory`	`disjointed` `Set` `BooleanAlgebra.toGeneralizedBooleanAlgebra` `Set.instBooleanAlgebra`	—	`disjointedRec` `isCaratheodory_diff`
`isCaratheodory_empty` 📖	mathematical	—	`IsCaratheodory` `Set` `Set.instEmptyCollection`	—	`Set.inter_empty` `MeasureTheory.measure_empty` `instOuterMeasureClass` `Set.diff_empty` `zero_add`
`isCaratheodory_iUnion` 📖	mathematical	`IsCaratheodory`	`Set.iUnion`	—	`iUnion_disjointed` `isCaratheodory_iUnion_of_disjoint` `isCaratheodory_disjointed` `disjoint_disjointed`
`isCaratheodory_iUnion_lt` 📖	mathematical	`IsCaratheodory`	`Set.iUnion`	—	`Set.iUnion_congr_Prop` `Nat.instCanonicallyOrderedAdd` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.biUnion_lt_succ` `isCaratheodory_union` `lt_of_lt_of_le` `le_refl`
`isCaratheodory_iUnion_of_disjoint` 📖	mathematical	`IsCaratheodory` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Set.iUnion`	—	`isCaratheodory_iff_le'` `Set.inter_iUnion` `ENNReal.tsum_eq_iSup_nat` `isCaratheodory_sum` `MeasureTheory.measure_iUnion_le` `instOuterMeasureClass` `instCountableNat` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `le_refl` `ENNReal.iSup_add` `iSup_le` `isCaratheodory_iUnion_lt` `add_le_add_right` `MeasureTheory.measure_mono` `Set.diff_subset_diff` `subset_refl` `Set.instReflSubset` `Set.iUnion_mono''` `Set.iUnion_subset` `Set.Subset.rfl`
`isCaratheodory_iff` 📖	mathematical	—	`MeasurableSet` `caratheodory` `DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Set.instInter` `Set.instSDiff`	—	—
`isCaratheodory_iff_le` 📖	mathematical	—	`MeasurableSet` `caratheodory` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `instFunLikeSetENNReal` `Set.instInter` `Set.instSDiff`	—	`isCaratheodory_iff_le'`
`isCaratheodory_iff_le'` 📖	mathematical	—	`IsCaratheodory` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `instFunLikeSetENNReal` `Set.instInter` `Set.instSDiff`	—	`le_antisymm_iff` `MeasureTheory.measure_le_inter_add_diff` `instOuterMeasureClass`
`isCaratheodory_inter` 📖	mathematical	`IsCaratheodory`	`Set` `Set.instInter`	—	`isCaratheodory_compl_iff` `Set.compl_inter` `isCaratheodory_union` `isCaratheodory_compl`
`isCaratheodory_partialSups` 📖	mathematical	`IsCaratheodory`	`DFunLike.coe` `OrderHom` `Set` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `OrderHom.instFunLike` `partialSups`	—	`Finset.nonempty_Iic` `Finset.sup'_eq_sup` `Finset.sup_set_eq_biUnion` `Set.iUnion_congr_Prop` `Finset.coe_Iic` `IsCaratheodory.biUnion_of_finite` `Set.finite_Iic`
`isCaratheodory_sum` 📖	mathematical	`IsCaratheodory` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.range` `DFunLike.coe` `MeasureTheory.OuterMeasure` `instFunLikeSetENNReal` `Set.instInter` `Set.iUnion`	—	`Set.iUnion_congr_Prop` `Nat.instCanonicallyOrderedAdd` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.inter_empty` `MeasureTheory.measure_empty` `instOuterMeasureClass` `Set.biUnion_lt_succ` `Finset.sum_range_succ` `Set.union_comm` `measure_inter_union` `Disjoint.le_bot` `ne_of_gt` `add_comm`
`isCaratheodory_union` 📖	mathematical	`IsCaratheodory`	`Set` `Set.instUnion`	—	`Set.inter_diff_assoc` `Set.inter_assoc` `Set.inter_eq_self_of_subset_right` `Set.subset_union_left` `Set.union_diff_left` `Set.inter_comm` `Set.inter_left_comm` `add_assoc` `Set.compl_union`
`le_add_caratheodory` 📖	mathematical	—	`MeasurableSpace` `MeasurableSpace.instLE` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `caratheodory` `MeasureTheory.OuterMeasure` `instAdd`	—	`add_left_comm` `add_assoc`
`le_smul_caratheodory` 📖	mathematical	—	`MeasurableSpace` `MeasurableSpace.instLE` `caratheodory` `ENNReal` `MeasureTheory.OuterMeasure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `isCaratheodory_iff` `mul_add` `Distrib.leftDistribClass`
`le_sum_caratheodory` 📖	mathematical	—	`MeasurableSpace` `MeasurableSpace.instLE` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `caratheodory` `sum`	—	`MeasurableSpace.measurableSet_iInf` `ENNReal.tsum_add`
`measure_inter_union` 📖	mathematical	`Set` `Set.instHasSubset` `Set.instInter` `Set.instEmptyCollection` `IsCaratheodory`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `ENNReal` `instFunLikeSetENNReal` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`Set.inter_assoc` `Set.union_inter_cancel_left` `Set.inter_diff_assoc` `Set.union_diff_cancel_left`
`ofFunction_caratheodory` 📖	mathematical	`Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Set.instInter` `Set.instSDiff`	`MeasurableSet` `caratheodory` `ofFunction`	—	`isCaratheodory_iff_le` `le_iInf` `le_trans` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `iInf_le_of_le` `iInf_le` `Set.iUnion_inter` `Set.inter_subset_inter_left` `Set.iUnion_diff` `Set.diff_subset_diff_left` `ENNReal.tsum_add` `ENNReal.tsum_le_tsum`
`top_caratheodory` 📖	mathematical	—	`caratheodory` `Top.top` `MeasureTheory.OuterMeasure` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `MeasurableSpace` `MeasurableSpace.instCompleteLattice`	—	`top_unique` `isCaratheodory_iff_le` `Set.eq_empty_or_nonempty` `Set.empty_inter` `MeasureTheory.measure_empty` `instOuterMeasureClass` `Set.empty_diff` `add_zero` `top_apply`
`zero_caratheodory` 📖	mathematical	—	`caratheodory` `MeasureTheory.OuterMeasure` `instZero` `Top.top` `MeasurableSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`top_unique` `add_zero`

MeasureTheory.OuterMeasure.IsCaratheodory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_of_finite` 📖	mathematical	`MeasureTheory.OuterMeasure.IsCaratheodory`	`Set.iUnion` `Set` `Set.instMembership`	—	`CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `Finset.induction_on` `Set.iUnion_congr_Prop` `Finset.coe_empty` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.iUnion_iUnion_eq_or_left` `MeasureTheory.OuterMeasure.isCaratheodory_union`

---

← Back to Index