Documentation Verification Report

Hahn

📁 Source: Mathlib/MeasureTheory/Measure/Decomposition/Hahn.lean

Statistics

Metric	Count
Definitions `IsHahnDecomposition`	1
Theorems `compl`, `ge_on_compl`, `le_on`, `measurableSet`, `exists_isHahnDecomposition`, `hahn_decomposition`	6
Total	7

MeasureTheory

Definitions

Name	Category	Theorems
`IsHahnDecomposition` 📖	CompData	1 math math: `exists_isHahnDecomposition`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isHahnDecomposition` 📖	mathematical	—	`IsHahnDecomposition`	—	`hahn_decomposition` `Measure.le_iff` `Measure.restrict_apply`
`hahn_decomposition` 📖	mathematical	—	`MeasurableSet` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike`	—	`measure_ne_top` `ENNReal.coe_toNNReal` `measure_inter_add_diff` `ENNReal.toNNReal_add` `NNReal.coe_add` `sub_eq_add_neg` `neg_add` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `NNReal.tendsto_coe` `Filter.Tendsto.comp` `ENNReal.tendsto_toNNReal` `tendsto_measure_iUnion_atTop` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `tendsto_measure_iInter_atTop` `MeasurableSet.nullMeasurableSet` `le_trans` `sub_le_self` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NNReal.coe_nonneg` `NNReal.coe_le_coe` `ENNReal.coe_le_coe` `measure_mono` `Measure.instOuterMeasureClass` `Set.subset_univ` `Set.Nonempty.image` `MeasurableSet.empty` `le_csSup` `Nat.instAtLeastTwoHAddOfNat` `sub_lt_self` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `zero_lt_one` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `exists_lt_of_lt_csSup` `Classical.axiom_of_choice` `Finset.inf_eq_iInf` `MeasurableSet.biInter` `Set.to_countable` `SetCoe.countable` `Set.biInter_subset_biInter_left` `Finset.Ico_subset_Ico` `le_of_lt` `Finset.insert_Ico_right_eq_Ico_add_one` `Nat.instNoMaxOrder` `Finset.inf_insert` `Set.inter_comm` `Nat.le_induction` `Nat.Ico_succ_singleton` `Finset.inf_singleton` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `CancelDenoms.sub_subst` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `CancelDenoms.add_subst` `CancelDenoms.mul_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `le_of_add_le_add_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `pow_succ` `mul_one_div` `sub_half` `CharZero.NeZero.two` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `add_le_add` `covariant_swap_add_of_covariant_add` `add_assoc` `le_refl` `Set.union_diff_left` `Set.union_inter_cancel_left` `le_imp_le_of_le_of_le` `add_le_add_left` `MeasurableSet.union` `tendsto_const_nhds` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_pow_atTop_nhds_zero_of_lt_one` `AddGroup.existsAddOfLE` `Real.instArchimedean` `instOrderTopologyReal` `half_lt_self` `MulZeroClass.mul_zero` `tsub_zero` `AddGroup.toOrderedSub` `Set.subset_iInter` `Set.Subset.trans` `Set.iInter_subset` `le_rfl` `le_of_tendsto_of_tendsto'` `OrderTopology.to_orderClosedTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `ge_of_tendsto` `instClosedIciTopology` `Filter.eventually_atTop` `le_add_of_le_of_nonneg` `pow_nonneg` `IsOrderedRing.toPosMulMono` `MeasurableSet.iUnion` `MeasurableSet.iInter` `add_le_add_iff_left` `Set.inter_eq_self_of_subset_right` `MeasurableSet.diff` `Set.union_diff_right` `Set.union_inter_cancel_right` `Disjoint.sdiff_eq_left` `Set.subset_compl_iff_disjoint_left`

MeasureTheory.IsHahnDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl` 📖	mathematical	`MeasureTheory.IsHahnDecomposition`	`Compl.compl` `Set` `Set.instCompl`	—	`MeasurableSet.compl` `measurableSet` `ge_on_compl` `compl_compl` `le_on`
`ge_on_compl` 📖	mathematical	`MeasureTheory.IsHahnDecomposition`	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.Measure.instPartialOrder` `MeasureTheory.Measure.restrict` `Compl.compl` `Set` `Set.instCompl`	—	—
`le_on` 📖	mathematical	`MeasureTheory.IsHahnDecomposition`	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.Measure.instPartialOrder` `MeasureTheory.Measure.restrict`	—	—
`measurableSet` 📖	mathematical	`MeasureTheory.IsHahnDecomposition`	`MeasurableSet`	—	—

---

← Back to Index