Documentation Verification Report

HasOuterApproxClosed

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

Statistics

Metric	Count
Definitions `HasOuterApproxClosed`, `apprSeq`	2
Theorems `apprSeq_apply_eq_one`, `apprSeq_apply_le_one`, `exAppr`, `indicator_le_apprSeq`, `measure_le_lintegral`, `tendsto_apprSeq`, `tendsto_lintegral_apprSeq`, `ext_of_forall_integral_eq_of_IsFiniteMeasure`, `ext_of_forall_lintegral_eq_of_IsFiniteMeasure`, `integrable_thickenedIndicator`, `measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure`, `measure_of_cont_bdd_of_tendsto_filter_indicator`, `measure_of_cont_bdd_of_tendsto_indicator`, `tendsto_integral_thickenedIndicator_of_isClosed`, `tendsto_lintegral_nn_filter_of_le_const`, `tendsto_lintegral_thickenedIndicator_of_isClosed`, `instHasOuterApproxClosedOfPseudoMetrizableSpace`	17
Total	19

HasOuterApproxClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apprSeq_apply_eq_one` 📖	mathematical	`Set` `Set.instMembership`	`DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `IsClosed.apprSeq` `instOneNNReal`	—	`le_antisymm` `apprSeq_apply_le_one` `exAppr`
`apprSeq_apply_le_one` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `IsClosed.apprSeq` `instOneNNReal`	—	`exAppr`
`exAppr` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `instOneNNReal` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `Pi.topologicalSpace` `NNReal.instTopologicalSpace` `Set.indicator` `instZeroNNReal`	—	—
`indicator_le_apprSeq` 📖	mathematical	—	`Pi.hasLe` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Set.indicator` `instZeroNNReal` `instOneNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `IsClosed.apprSeq`	—	`Set.indicator_of_mem` `apprSeq_apply_eq_one` `Set.indicator_of_notMem` `NNReal.instCanonicallyOrderedAdd`
`measure_le_lintegral` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.lintegral` `ENNReal.ofNNReal` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `IsClosed.apprSeq`	—	`MeasureTheory.lintegral_indicator` `IsClosed.measurableSet` `MeasureTheory.lintegral_one` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `MeasureTheory.lintegral_mono` `Set.indicator_of_mem` `apprSeq_apply_eq_one` `Set.indicator_of_notMem` `ENNReal.instCanonicallyOrderedAdd`
`tendsto_apprSeq` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `IsClosed.apprSeq` `Filter.atTop` `Nat.instPreorder` `nhds` `Pi.topologicalSpace` `NNReal.instTopologicalSpace` `Set.indicator` `instZeroNNReal` `instOneNNReal`	—	`exAppr`
`tendsto_lintegral_apprSeq` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `MeasureTheory.lintegral` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `IsClosed.apprSeq` `Filter.atTop` `Nat.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	—	`MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator` `IsClosed.measurableSet` `apprSeq_apply_le_one` `tendsto_apprSeq`

IsClosed

Definitions

Name	Category	Theorems
`apprSeq` 📖	CompOp	6 math math: `HasOuterApproxClosed.tendsto_apprSeq`, `HasOuterApproxClosed.measure_le_lintegral`, `HasOuterApproxClosed.apprSeq_apply_eq_one`, `HasOuterApproxClosed.tendsto_lintegral_apprSeq`, `HasOuterApproxClosed.indicator_le_apprSeq`, `HasOuterApproxClosed.apprSeq_apply_le_one`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_of_forall_integral_eq_of_IsFiniteMeasure` 📖	—	`integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `BoundedContinuousFunction.instFunLike`	—	—	`ext_of_forall_lintegral_eq_of_IsFiniteMeasure` `ENNReal.toReal_eq_toReal_iff'` `LT.lt.ne` `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` `BoundedContinuousFunction.toReal_lintegral_coe_eq_integral` `BorelSpace.opensMeasurable` `Continuous.comp'` `NNReal.continuous_coe` `BoundedContinuousFunction.continuous` `BoundedContinuousFunction.map_bounded'`
`ext_of_forall_lintegral_eq_of_IsFiniteMeasure` 📖	—	`lintegral` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	—	—	`measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure` `BorelSpace.opensMeasurable` `ext_of_generate_finite` `BorelSpace.measurable_eq` `borel_eq_generateFrom_isClosed` `isPiSystem_isClosed` `isClosed_univ`
`integrable_thickenedIndicator` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NNReal.toReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `PseudoEMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `thickenedIndicator`	—	`Integrable.of_bound` `Continuous.comp_aestronglyMeasurable` `NNReal.continuous_coe` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `NNReal.instSecondCountableTopology` `ContinuousMapClass.map_continuous` `BoundedContinuousMapClass.toContinuousMapClass` `BoundedContinuousFunction.instBoundedContinuousMapClass` `ae_of_all` `Measure.instOuterMeasureClass` `NNReal.abs_eq` `thickenedIndicator_le_one`
`measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure` 📖	mathematical	`lintegral` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	`Measure` `Set` `ENNReal` `Measure.instFunLike`	—	`lintegral_const` `one_mul` `HasOuterApproxClosed.tendsto_lintegral_apprSeq` `tendsto_nhds_unique` `ENNReal.instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`measure_of_cont_bdd_of_tendsto_filter_indicator` 📖	mathematical	`MeasurableSet` `Filter.Eventually` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Filter.Tendsto` `nhds` `NNReal.instTopologicalSpace` `Set.indicator` `instZeroNNReal` `instOneNNReal`	`ENNReal` `lintegral` `ENNReal.ofNNReal` `ENNReal.instTopologicalSpace` `Set`	—	`Measure.instOuterMeasureClass` `ENNReal.coe_indicator` `lintegral_indicator` `lintegral_one` `Measure.restrict_apply` `Set.univ_inter` `tendsto_lintegral_nn_filter_of_le_const`
`measure_of_cont_bdd_of_tendsto_indicator` 📖	mathematical	`MeasurableSet` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `Pi.topologicalSpace` `NNReal.instTopologicalSpace` `Set.indicator` `instZeroNNReal` `instOneNNReal`	`ENNReal` `lintegral` `ENNReal.ofNNReal` `ENNReal.instTopologicalSpace` `Measure` `Set` `Measure.instFunLike`	—	`tendsto_pi_nhds` `measure_of_cont_bdd_of_tendsto_filter_indicator` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`tendsto_integral_thickenedIndicator_of_isClosed` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `NNReal.toReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `PseudoEMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `thickenedIndicator` `Measure.real`	—	`tendsto_lintegral_thickenedIndicator_of_isClosed` `lintegral_coe_eq_integral` `integrable_thickenedIndicator` `Measure.real_def` `ENNReal.toReal_ofReal` `integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `ENNReal.tendsto_toReal_iff` `measure_ne_top`
`tendsto_lintegral_nn_filter_of_le_const` 📖	mathematical	`Filter.Eventually` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Filter.Tendsto` `nhds` `NNReal.instTopologicalSpace`	`ENNReal` `lintegral` `ENNReal.ofNNReal` `ENNReal.instTopologicalSpace`	—	`Measure.instOuterMeasureClass` `tendsto_lintegral_filter_of_dominated_convergence` `Filter.Eventually.of_forall` `Continuous.measurable` `ENNReal.borelSpace` `Continuous.comp` `ENNReal.continuous_coe` `BoundedContinuousFunction.continuous` `LT.lt.ne` `lintegral_const_lt_top` `ENNReal.coe_ne_top`
`tendsto_lintegral_thickenedIndicator_of_isClosed` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`ENNReal` `lintegral` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `PseudoEMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `thickenedIndicator` `ENNReal.instTopologicalSpace` `Measure` `Set` `Measure.instFunLike`	—	`measure_of_cont_bdd_of_tendsto_indicator` `IsClosed.measurableSet` `thickenedIndicator_le_one` `thickenedIndicator_tendsto_indicator_closure` `IsClosed.closure_eq`

(root)

Definitions

Name	Category	Theorems
`HasOuterApproxClosed` 📖	CompData	1 math math: `instHasOuterApproxClosedOfPseudoMetrizableSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasOuterApproxClosedOfPseudoMetrizableSpace` 📖	mathematical	—	`HasOuterApproxClosed`	—	`Nat.one_div_pos_of_nat` `Real.instIsStrictOrderedRing` `thickenedIndicator_le_one` `one_le_thickenedIndicator_apply` `thickenedIndicator_tendsto_indicator_closure` `tendsto_one_div_add_atTop_nhds_zero_nat` `RCLike.charZero_rclike` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal` `tendsto_pi_nhds` `IsClosed.closure_eq`

---

← Back to Index