Documentation Verification Report

FiniteMeasureExt

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

Statistics

Metric	Count
Definitions	0
Theorems `ext_of_forall_mem_subalgebra_integral_eq_of_polish`, `ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable`	2
Total	2

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_of_forall_mem_subalgebra_integral_eq_of_polish` 📖	—	`Subalgebra.SeparatesPoints` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedAlgebra.id` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `StarSubalgebra.toSubalgebra` `ContinuousMap` `RCLike.toStarRing` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.instStarRingOfContinuousStar` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `ContinuousMap.algebra` `ContinuousMap.instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `StarRing.toStarAddMonoid` `Algebra.toSMul` `StarMul.toStarModule` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `StarRing.toStarMul` `CommRing.toRing` `StarSubalgebra.map` `BoundedContinuousFunction` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `BoundedContinuousFunction.instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instBoundedMul` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `BoundedContinuousFunction.instStarRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `BoundedContinuousFunction.instAlgebra` `BoundedContinuousFunction.instStarModule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `BoundedContinuousFunction.toContinuousMapStarₐ` `integral` `Real` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `BoundedContinuousFunction.instFunLike`	—	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `BoundedContinuousFunction.instStarModule` `StarMul.toStarModule` `NonUnitalSeminormedRing.toIsTopologicalRing` `RCLike.instContinuousStar` `ContinuousMap.instStarModule` `ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable` `PolishSpace.toIsCompletelyMetrizableSpace` `TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace` `PolishSpace.toSecondCountableTopology`
`ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable` 📖	—	`Subalgebra.SeparatesPoints` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedAlgebra.id` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `StarSubalgebra.toSubalgebra` `ContinuousMap` `RCLike.toStarRing` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.instStarRingOfContinuousStar` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `ContinuousMap.algebra` `ContinuousMap.instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `StarRing.toStarAddMonoid` `Algebra.toSMul` `StarMul.toStarModule` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `StarRing.toStarMul` `CommRing.toRing` `StarSubalgebra.map` `BoundedContinuousFunction` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `BoundedContinuousFunction.instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instBoundedMul` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `BoundedContinuousFunction.instStarRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `BoundedContinuousFunction.instAlgebra` `BoundedContinuousFunction.instStarModule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `BoundedContinuousFunction.toContinuousMapStarₐ` `integral` `Real` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `BoundedContinuousFunction.instFunLike`	—	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `BoundedContinuousFunction.instStarModule` `StarMul.toStarModule` `NonUnitalSeminormedRing.toIsTopologicalRing` `RCLike.instContinuousStar` `ContinuousMap.instStarModule` `RCLike.lipschitzWith_ofReal` `BoundedContinuousFunction.instIsScalarTower` `IsScalarTower.right` `instIsTopologicalRingReal` `RCLike.continuous_ofReal` `ContinuousMap.instIsScalarTower` `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict` `Subalgebra.SeparatesPoints.rclike_to_real` `integral_ofReal` `ext_of_forall_integral_eq_of_IsFiniteMeasure` `instHasOuterApproxClosedOfPseudoMetrizableSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `Nat.instAtLeastTwoHAddOfNat` `MulZeroClass.mul_zero` `tendsto_nhdsWithin_of_tendsto_nhds` `Filter.Tendsto.const_mul` `Real.sqrt_zero` `Continuous.tendsto` `Real.continuous_sqrt` `squeeze_zero'` `eventually_nhdsWithin_of_forall` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `dist_integral_mulExpNegMulSq_comp_le` `Filter.Tendsto.abs` `instOrderTopologyReal` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `tendsto_integral_mulExpNegMulSq_comp` `eq_of_abs_sub_eq_zero` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `nhdsGT_neBot` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`

---

← Back to Index