Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `OuterMeasure`, `instFunLikeSetENNReal`, `measureOf`, `OuterMeasureClass`	4
Theorems `empty`, `iUnion_nat`, `instOuterMeasureClass`, `measureOf_eq_coe`, `mono`, `measure_empty`, `measure_iUnion_nat_le`, `measure_mono`	8
Total	12

MeasureTheory

Definitions

Name	Category	Theorems
`OuterMeasure` 📖	CompData	224 math math: `OuterMeasure.map_iInf`, `Content.is_add_left_invariant_outerMeasure`, `PMF.toOuterMeasure_mono`, `OuterMeasure.instLawfulFunctor`, `OuterMeasure.mkMetric_top`, `OuterMeasure.comap_map`, `OuterMeasure.le_boundedBy'`, `PMF.toOuterMeasure_pure_apply`, `Measure.outerMeasure_le_iff`, `Measure.haarMeasure_apply`, `OuterMeasure.restrict_trim`, `OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top`, `OuterMeasure.trim_top`, `OuterMeasure.coe_iSup`, `OuterMeasure.trim_smul`, `PMF.toOuterMeasure_injective`, `Measure.haar.addHaarContent_outerMeasure_self_pos`, `inducedOuterMeasure_caratheodory`, `Content.le_outerMeasure_compacts`, `OuterMeasure.comap_iInf`, `Measure.haar.addHaarContent_outerMeasure_closure_pos`, `PMF.toOuterMeasure_ofFinset_apply`, `inducedOuterMeasure_eq'`, `Content.is_mul_left_invariant_outerMeasure`, `OuterMeasure.map_apply`, `OuterMeasure.le_pi`, `OuterMeasure.isCaratheodory_iff_le'`, `OuterMeasure.iInf_apply'`, `Measure.sInf_caratheodory`, `OuterMeasure.restrict_iInf`, `OuterMeasure.comap_apply`, `PMF.toOuterMeasure_apply_eq_of_inter_support_eq`, `OuterMeasure.restrict_ofFunction`, `Measure.toOuterMeasure_apply`, `OuterMeasure.map_iInf_comap`, `OuterMeasure.isCaratheodory_iff`, `Content.outerMeasure_preimage`, `OuterMeasure.map_comap_le`, `OuterMeasure.trim_sup`, `OuterMeasure.coe_add`, `OuterMeasure.map_le_restrict_range`, `OuterMeasure.trim_zero`, `Measure.zero_toOuterMeasure`, `Content.outerMeasure_interior_compacts`, `OuterMeasure.isometry_comap_mkMetric`, `OuterMeasure.map_comap`, `Measure.coe_toOuterMeasure`, `OuterMeasure.trim_eq_iInf'`, `OuterMeasure.restrict_univ`, `Content.outerMeasure_eq_iInf`, `OuterMeasure.mkMetric'.tendsto_pre`, `PMF.toMeasure_apply_eq_toOuterMeasure_apply`, `inducedOuterMeasure_preimage`, `OuterMeasure.map_iInf_le`, `PMF.toOuterMeasure_apply_le_toMeasure_apply`, `le_inducedOuterMeasure`, `OuterMeasure.add_apply`, `OuterMeasure.boundedBy_eq`, `OuterMeasure.trim_le_trim_iff`, `Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict`, `PMF.toOuterMeasure_apply_singleton`, `OuterMeasure.comap_top`, `OuterMeasure.iInf_apply`, `OuterMeasure.exists_measurable_superset_forall_eq_trim`, `OuterMeasure.dirac_apply`, `Measure.smul_toOuterMeasure`, `OuterMeasure.trim_anti_measurableSpace`, `OuterMeasure.map_map`, `OuterMeasure.biInf_apply`, `OuterMeasure.le_add_caratheodory`, `OuterMeasure.restrict_empty`, `OuterMeasure.mkMetric'.tendsto_pre_nat`, `AddContent.ofFunction_eq`, `Content.outerMeasure_le`, `OuterMeasure.map_ofFunction`, `OuterMeasure.map_comap_of_surjective`, `OuterMeasure.zero_caratheodory`, `OuterMeasure.boundedBy_le`, `PMF.toOuterMeasure_ofMultiset_apply`, `OuterMeasure.top_caratheodory`, `Measure.addHaarMeasure_apply`, `inducedOuterMeasure_exists_set`, `Measure.m_iUnion`, `OuterMeasure.sup_apply`, `OuterMeasure.instSMulCommClass`, `OuterMeasure.ofFunction_eq_iInf_mem`, `Measure.sInf_apply`, `OuterMeasure.map_iSup`, `OuterMeasure.trim_sum_ge`, `OuterMeasure.restrict_iSup`, `OuterMeasure.isCaratheodory_iff_le`, `OuterMeasure.instIsCentralScalar`, `PMF.toOuterMeasure_ofFintype_apply`, `Content.outerMeasure_pos_of_is_mul_left_invariant`, `OuterMeasure.coe_fn_injective`, `PMF.toOuterMeasure_uniformOfFinset_apply`, `inducedOuterMeasure_eq_iInf`, `OuterMeasure.comap_mono`, `OuterMeasure.boundedBy_eq_self`, `PMF.toOuterMeasure_bindOnSupport_apply`, `OuterMeasure.le_comap_map`, `Measure.toOuterMeasure_injective`, `OuterMeasure.le_trim`, `OuterMeasure.sSup_apply`, `OuterMeasure.mkMetric'.pre_le`, `OuterMeasure.ext_iff`, `Content.outerMeasure_exists_open`, `OuterMeasure.boundedBy_zero`, `OuterMeasure.measure_inter_union`, `OuterMeasure.coeFnAddMonoidHom_apply`, `piPremeasure_pi'`, `OuterMeasure.coe_zero`, `OuterMeasure.le_smul_caratheodory`, `OuterMeasure.pi_pi_le`, `OuterMeasure.measureOf_eq_coe`, `le_toMeasure_apply`, `OuterMeasure.mkMetric'.mono_pre_nat`, `Measure.map_toOuterMeasure`, `toMeasure_apply₀`, `AddContent.inducedOuterMeasure_eq`, `inducedOuterMeasure_eq_extend`, `Content.outerMeasure_caratheodory`, `OuterMeasure.coe_bot`, `OuterMeasure.le_trim_iff`, `Content.outerMeasure_exists_compact`, `OuterMeasure.isometryEquiv_map_mkMetric`, `piPremeasure_pi`, `PMF.toOuterMeasure_apply_inter_support`, `OuterMeasure.boundedBy_apply`, `StieltjesFunction.outer_le_length`, `OuterMeasure.restrict_biInf`, `OuterMeasure.ofFunction_union_of_top_of_nonempty_inter`, `OuterMeasure.boundedBy_top`, `Measure.toOuterMeasure_le`, `OuterMeasure.isCaratheodory_sum`, `OuterMeasure.smul_boundedBy`, `PMF.toOuterMeasure_map_apply`, `OuterMeasure.isGreatest_ofFunction`, `OuterMeasure.boundedBy_eq_ofFunction`, `inducedOuterMeasure_eq`, `OuterMeasure.ofFunction_le`, `Content.outerMeasure_opens`, `OuterMeasure.comap_boundedBy`, `OuterMeasure.map_id`, `OuterMeasure.isometry_map_mkMetric`, `OuterMeasure.smul_iSup`, `OuterMeasure.trim_mono`, `inducedOuterMeasure_union_of_false_of_nonempty_inter`, `Content.outerMeasure_pos_of_is_add_left_invariant`, `OuterMeasure.top_apply'`, `OuterMeasure.ofFunction_eq`, `OuterMeasure.mkMetric'.mono_pre`, `OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated`, `OuterMeasure.trim_eq`, `Measure.toOuterMeasure_top`, `OuterMeasure.sInf_apply'`, `measure_eq_inducedOuterMeasure`, `toMeasure_apply`, `AddContent.measureCaratheodory_eq_inducedOuterMeasure`, `OuterMeasure.sum_apply`, `StieltjesFunction.outer_Ioc`, `OuterMeasure.coe_mkMetric`, `PMF.toOuterMeasure_apply`, `OuterMeasure.mkMetric'.eq_iSup_nat`, `PMF.toOuterMeasure_apply_eq_zero_iff`, `OuterMeasure.instOuterMeasureClass`, `OuterMeasure.trim_add`, `OuterMeasure.map_top_of_surjective`, `OuterMeasure.restrict_apply`, `OuterMeasure.instIsOrderedAddMonoid`, `OuterMeasure.mkMetric_mono`, `OuterMeasure.sInf_eq_boundedBy_sInfGen`, `OuterMeasure.mkMetric_smul`, `OuterMeasure.sInfGen_def`, `measure_eq_trim`, `OuterMeasure.boundedBy_union_of_top_of_nonempty_inter`, `OuterMeasure.map_top`, `OuterMeasure.trim_eq_trim_iff`, `PMF.toOuterMeasure_apply_finset`, `OuterMeasure.biInf_apply'`, `OuterMeasure.iSup_apply`, `Measure.trim_le`, `OuterMeasure.ofFunction_eq_sSup`, `OuterMeasure.f_iUnion`, `OuterMeasure.le_boundedBy`, `OuterMeasure.smul_dirac_apply`, `Measure.haar.haarContent_outerMeasure_closure_pos`, `OuterMeasure.top_apply`, `OuterMeasure.exists_measurable_superset_eq_trim`, `OuterMeasure.trim_eq_iInf`, `PMF.toOuterMeasure_apply_eq_one_iff`, `OuterMeasure.iUnion_eq_of_caratheodory`, `OuterMeasure.mkMetric_nnreal_smul`, `OuterMeasure.comap_iSup`, `Content.outerMeasure_lt_top_of_isCompact`, `OuterMeasure.le_ofFunction`, `OuterMeasure.smul_ofFunction`, `OuterMeasure.map_biInf_comap`, `Measure.haar.haarContent_outerMeasure_self_pos`, `PMF.toOuterMeasure_uniformOfFintype_apply`, `PMF.toOuterMeasure_bind_apply`, `OuterMeasure.trim_iSup`, `OuterMeasure.instIsScalarTower`, `OuterMeasure.toMeasure_eq_zero`, `OuterMeasure.restrict_iInf_restrict`, `OuterMeasure.ofFunction_apply`, `PMF.toMeasure_apply_eq_toOuterMeasure`, `OuterMeasure.map_ofFunction_le`, `OuterMeasure.map_sup`, `OuterMeasure.coe_smul`, `OuterMeasure.univ_eq_zero_iff`, `OuterMeasure.comap_ofFunction`, `Measure.add_toOuterMeasure`, `Content.outerMeasure_of_isOpen`, `OuterMeasure.map_mono`, `OuterMeasure.restrict_le_self`, `OuterMeasure.smul_apply`, `Content.measure_apply`, `OuterMeasure.toMeasure_top`, `OuterMeasure.mkMetric_mono_smul`, `OuterMeasure.mkMetric'.le_pre`, `inducedOuterMeasure_eq_extend'`, `PMF.toOuterMeasure_apply_fintype`, `OuterMeasure.isometryEquiv_comap_mkMetric`
`OuterMeasureClass` 📖	CompData	2 math math: `OuterMeasure.instOuterMeasureClass`, `Measure.instOuterMeasureClass`

MeasureTheory.OuterMeasure

Definitions

Name	Category	Theorems
`instFunLikeSetENNReal` 📖	CompOp	143 math math: `MeasureTheory.Content.is_add_left_invariant_outerMeasure`, `PMF.toOuterMeasure_mono`, `le_boundedBy'`, `PMF.toOuterMeasure_pure_apply`, `MeasureTheory.Measure.outerMeasure_le_iff`, `mono''`, `MeasureTheory.Measure.haarMeasure_apply`, `iUnion_nat_of_monotone_of_tsum_ne_top`, `coe_iSup`, `MeasureTheory.Measure.haar.addHaarContent_outerMeasure_self_pos`, `MeasureTheory.inducedOuterMeasure_caratheodory`, `MeasureTheory.Content.le_outerMeasure_compacts`, `MeasureTheory.Measure.haar.addHaarContent_outerMeasure_closure_pos`, `PMF.toOuterMeasure_ofFinset_apply`, `MeasureTheory.inducedOuterMeasure_eq'`, `MeasureTheory.Content.is_mul_left_invariant_outerMeasure`, `map_apply`, `le_pi`, `isCaratheodory_iff_le'`, `iInf_apply'`, `comap_apply`, `PMF.toOuterMeasure_apply_eq_of_inter_support_eq`, `MeasureTheory.Measure.toOuterMeasure_apply`, `isCaratheodory_iff`, `MeasureTheory.Content.outerMeasure_preimage`, `coe_add`, `MeasureTheory.Content.outerMeasure_interior_compacts`, `MeasureTheory.Measure.coe_toOuterMeasure`, `trim_eq_iInf'`, `MeasureTheory.Measure.liftLinear_apply₀`, `MeasureTheory.Content.outerMeasure_eq_iInf`, `mkMetric'.tendsto_pre`, `PMF.toMeasure_apply_eq_toOuterMeasure_apply`, `MeasureTheory.inducedOuterMeasure_preimage`, `PMF.toOuterMeasure_apply_le_toMeasure_apply`, `MeasureTheory.le_inducedOuterMeasure`, `add_apply`, `boundedBy_eq`, `trim_le_trim_iff`, `PMF.toOuterMeasure_apply_singleton`, `iInf_apply`, `exists_measurable_superset_forall_eq_trim`, `dirac_apply`, `biInf_apply`, `mkMetric'.tendsto_pre_nat`, `MeasureTheory.AddContent.ofFunction_eq`, `MeasureTheory.Content.outerMeasure_le`, `boundedBy_le`, `PMF.toOuterMeasure_ofMultiset_apply`, `MeasureTheory.Measure.addHaarMeasure_apply`, `MeasureTheory.inducedOuterMeasure_exists_set`, `MeasureTheory.Measure.m_iUnion`, `sup_apply`, `ofFunction_eq_iInf_mem`, `MeasureTheory.Measure.sInf_apply`, `isCaratheodory_iff_le`, `PMF.toOuterMeasure_ofFintype_apply`, `MeasureTheory.Content.outerMeasure_pos_of_is_mul_left_invariant`, `coe_fn_injective`, `PMF.toOuterMeasure_uniformOfFinset_apply`, `MeasureTheory.inducedOuterMeasure_eq_iInf`, `MeasureTheory.Measure.le_liftLinear_apply`, `boundedBy_eq_self`, `PMF.toOuterMeasure_bindOnSupport_apply`, `sSup_apply`, `mkMetric'.pre_le`, `ext_iff`, `MeasureTheory.Content.outerMeasure_exists_open`, `measure_inter_union`, `coeFnAddMonoidHom_apply`, `MeasureTheory.piPremeasure_pi'`, `coe_zero`, `pi_pi_le`, `measureOf_eq_coe`, `MeasureTheory.le_toMeasure_apply`, `MeasureTheory.toMeasure_apply₀`, `MeasureTheory.AddContent.inducedOuterMeasure_eq`, `MeasureTheory.inducedOuterMeasure_eq_extend`, `sInf_apply`, `MeasureTheory.Content.outerMeasure_caratheodory`, `le_trim_iff`, `MeasureTheory.Content.outerMeasure_exists_compact`, `MeasureTheory.piPremeasure_pi`, `PMF.toOuterMeasure_apply_inter_support`, `boundedBy_apply`, `MeasureTheory.Measure.liftLinear_apply`, `StieltjesFunction.outer_le_length`, `ofFunction_union_of_top_of_nonempty_inter`, `isCaratheodory_sum`, `PMF.toOuterMeasure_map_apply`, `boundedBy_eq_ofFunction`, `MeasureTheory.inducedOuterMeasure_eq`, `ofFunction_le`, `MeasureTheory.Content.outerMeasure_opens`, `MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter`, `MeasureTheory.Content.outerMeasure_pos_of_is_add_left_invariant`, `top_apply'`, `ofFunction_eq`, `IsMetric.finset_iUnion_of_pairwise_separated`, `trim_eq`, `sInf_apply'`, `MeasureTheory.measure_eq_inducedOuterMeasure`, `MeasureTheory.toMeasure_apply`, `MeasureTheory.AddContent.measureCaratheodory_eq_inducedOuterMeasure`, `sum_apply`, `StieltjesFunction.outer_Ioc`, `coe_mkMetric`, `PMF.toOuterMeasure_apply`, `PMF.toOuterMeasure_apply_eq_zero_iff`, `instOuterMeasureClass`, `restrict_apply`, `sInfGen_def`, `MeasureTheory.measure_eq_trim`, `boundedBy_union_of_top_of_nonempty_inter`, `trim_eq_trim_iff`, `PMF.toOuterMeasure_apply_finset`, `biInf_apply'`, `iSup_apply`, `f_iUnion`, `le_boundedBy`, `smul_dirac_apply`, `MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos`, `top_apply`, `exists_measurable_superset_eq_trim`, `trim_eq_iInf`, `PMF.toOuterMeasure_apply_eq_one_iff`, `iUnion_eq_of_caratheodory`, `MeasureTheory.Content.outerMeasure_lt_top_of_isCompact`, `le_ofFunction`, `MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos`, `PMF.toOuterMeasure_uniformOfFintype_apply`, `PMF.toOuterMeasure_bind_apply`, `ofFunction_apply`, `PMF.toMeasure_apply_eq_toOuterMeasure`, `coe_smul`, `univ_eq_zero_iff`, `MeasureTheory.Content.outerMeasure_of_isOpen`, `smul_apply`, `MeasureTheory.Content.measure_apply`, `iSup_sInfGen_nonempty`, `mkMetric'.le_pre`, `MeasureTheory.inducedOuterMeasure_eq_extend'`, `PMF.toOuterMeasure_apply_fintype`
`measureOf` 📖	CompOp	4 math math: `empty`, `mono`, `iUnion_nat`, `measureOf_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty` 📖	mathematical	—	`measureOf` `Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	—	—
`iUnion_nat` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `measureOf` `Set.iUnion` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	—
`instOuterMeasureClass` 📖	mathematical	—	`MeasureTheory.OuterMeasureClass` `MeasureTheory.OuterMeasure` `instFunLikeSetENNReal`	—	`empty` `mono` `iUnion_nat`
`measureOf_eq_coe` 📖	mathematical	—	`measureOf` `DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `instFunLikeSetENNReal`	—	—
`mono` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `measureOf`	—	—

MeasureTheory.OuterMeasureClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measure_empty` 📖	mathematical	—	`DFunLike.coe` `Set` `ENNReal` `Set.instEmptyCollection` `instZeroENNReal`	—	—
`measure_iUnion_nat_le` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Set.iUnion` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	—
`measure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe`	—	—

---

← Back to Index