Documentation Verification Report

Sub

📁 Source: Mathlib/MeasureTheory/Measure/Sub.lean

Statistics

Metric	Count
Definitions `instSub`	1
Theorems `add_sub_cancel`, `isFiniteMeasure_sub`, `restrict_sub_eq_restrict_sub_restrict`, `sub_add_cancel_of_le`, `sub_apply`, `sub_apply_eq_zero_of_restrict_le_restrict`, `sub_def`, `sub_eq_zero_of_le`, `sub_le`, `sub_le_iff_le_add_of_le`, `sub_le_of_le_add`, `sub_self`, `sub_top`, `sub_zero`, `zero_sub`	15
Total	16

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`instSub` 📖	CompOp	27 math math: `sub_top`, `jordanDecompositionOfToSignedMeasureSub_posPart`, `sub_toSignedMeasure_eq_toSignedMeasure_sub`, `measure_sub_singularPart`, `mutually_singular_measure_sub`, `sub_le_iff_le_add`, `sub_le_iff_le_add_of_le`, `sub_add_cancel_of_le`, `add_sub_cancel`, `withDensity_sub_of_le`, `jordanDecompositionOfToSignedMeasureSub_negPart`, `sub_apply`, `sub_eq_zero_of_le`, `sub_le_of_le_add`, `sub_apply_eq_zero_of_isHahnDecomposition`, `restrict_sub_eq_restrict_sub_restrict`, `sub_def`, `zero_sub`, `measure_sub_rnDeriv`, `sub_le`, `sub_self`, `add_sub_of_mutuallySingular`, `isFiniteMeasure_sub`, `sub_apply_eq_zero_of_restrict_le_restrict`, `toSignedMeasure_restrict_sub`, `withDensity_sub`, `sub_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_sub_cancel` 📖	mathematical	—	`MeasureTheory.Measure` `instSub` `instAdd`	—	`ext` `sub_apply` `le_add_left` `le_refl` `add_apply` `ENNReal.add_sub_cancel_right` `MeasureTheory.measure_ne_top`
`isFiniteMeasure_sub` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `MeasureTheory.Measure` `instSub`	—	`MeasureTheory.isFiniteMeasure_of_le` `sub_le`
`restrict_sub_eq_restrict_sub_restrict` 📖	mathematical	`MeasurableSet`	`restrict` `MeasureTheory.Measure` `instSub`	—	`sub_def` `le_add_right` `le_rfl` `restrict_sInf_eq_sInf_restrict` `le_antisymm` `sInf_le_sInf_of_isCoinitialFor` `Set.mem_setOf_eq` `add_right_comm` `le_iff` `MeasureTheory.measure_inter_add_diff` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `add_apply` `le_add_right` `ENNReal.instCanonicallyOrderedAdd` `restrict_eq_self` `Set.inter_subset_right` `restrict_apply` `MeasurableSet.diff` `Set.diff_eq` `Set.inter_assoc` `Set.inter_self` `add_top` `le_iff'` `ext` `restrict_add` `MeasurableSet.inter` `Set.inter_compl_self` `Set.inter_empty` `MeasureTheory.measure_empty` `instOuterMeasureClass` `add_zero` `restrict_le_self` `Set.forall_mem_image` `restrict_mono` `Set.Subset.rfl`
`sub_add_cancel_of_le` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`MeasureTheory.Measure` `instAdd` `instSub`	—	`ext` `add_apply` `sub_apply` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `ENNReal.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `ENNReal.instOrderedSub`
`sub_apply` 📖	mathematical	`MeasurableSet` `MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `instSub` `ENNReal.instSub`	—	`MeasurableSet.empty` `MeasureTheory.measure_empty` `instOuterMeasureClass` `tsub_self` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `MeasurableSet.iUnion` `instCountableNat` `MeasureTheory.measure_iUnion` `ENNReal.tsum_sub` `MeasureTheory.measure_ne_top` `ext` `ofMeasurable_apply` `add_comm` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `sub_def` `le_antisymm` `sInf_le` `instReflLe` `le_sInf` `le_of_add_le_add_left` `Set.mem_setOf_eq`
`sub_apply_eq_zero_of_restrict_le_restrict` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `restrict` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `instSub` `instZeroENNReal`	—	`restrict_apply_self` `restrict_sub_eq_restrict_sub_restrict` `sub_eq_zero_of_le`
`sub_def` 📖	mathematical	—	`MeasureTheory.Measure` `instSub` `InfSet.sInf` `instInfSet` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instAdd`	—	—
`sub_eq_zero_of_le` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`MeasureTheory.Measure` `instSub` `instZero`	—	`nonpos_iff_eq_zero'` `sub_le_of_le_add` `zero_add`
`sub_le` 📖	mathematical	—	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instSub`	—	`sub_le_of_le_add` `le_add_right` `le_rfl`
`sub_le_iff_le_add_of_le` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instSub` `instAdd`	—	`le_iff` `tsub_le_iff_right` `ENNReal.instOrderedSub` `sub_apply` `sub_le_of_le_add`
`sub_le_of_le_add` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instAdd`	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instSub`	—	`sInf_le`
`sub_self` 📖	mathematical	—	`MeasureTheory.Measure` `instSub` `instZero`	—	`sub_eq_zero_of_le` `le_rfl`
`sub_top` 📖	mathematical	—	`MeasureTheory.Measure` `instSub` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `instZero`	—	`sub_eq_zero_of_le` `le_top`
`sub_zero` 📖	mathematical	—	`MeasureTheory.Measure` `instSub` `instZero`	—	`sub_def` `le_antisymm` `add_zero` `instReflLe`
`zero_sub` 📖	mathematical	—	`MeasureTheory.Measure` `instSub` `instZero`	—	`sub_eq_zero_of_le` `zero_le`

---

← Back to Index