Documentation Verification Report

Extension

📁 Source: Mathlib/MeasureTheory/Measure/Haar/Extension.lean

Statistics

Metric	Count
Definitions `inducedMeasure`, `integrate`, `pullback`, `pushforward`, `inducedMeasure`, `integrate`, `pullback`, `pushforward`	8
Theorems `inducedMeasure_lt_of_injOn`, `inducedMeasure_regular`, `integral_inducedMeasure`, `integral_pullback_invFun_apply`, `integrate_apply`, `integrate_mono`, `isAddHaarMeasure_inducedMeasure`, `pullback_def`, `pushforward_apply_apply`, `pushforward_def`, `pushforward_mono`, `inducedMeasure_lt_of_injOn`, `inducedMeasure_regular`, `integral_inducedMeasure`, `integral_pullback_invFun_apply`, `integrate_apply`, `integrate_mono`, `isHaarMeasure_inducedMeasure`, `pullback_def`, `pushforward_apply_apply`, `pushforward_def`, `pushforward_mono`	22
Total	30

TopologicalAddGroup.IsSES

Definitions

Name	Category	Theorems
`inducedMeasure` 📖	CompOp	4 math math: `isAddHaarMeasure_inducedMeasure`, `inducedMeasure_lt_of_injOn`, `integral_inducedMeasure`, `inducedMeasure_regular`
`integrate` 📖	CompOp	3 math math: `integrate_mono`, `integral_inducedMeasure`, `integrate_apply`
`pullback` 📖	CompOp	4 math math: `pushforward_apply_apply`, `integral_pullback_invFun_apply`, `pushforward_def`, `pullback_def`
`pushforward` 📖	CompOp	4 math math: `pushforward_apply_apply`, `pushforward_def`, `pushforward_mono`, `integrate_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inducedMeasure_lt_of_injOn` 📖	mathematical	`TopologicalAddGroup.IsSES` `IsOpen` `Set.InjOn` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `inducedMeasure` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Set.univ` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `not_le` `IsOpen.measure_pos` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `isOpen_discrete` `Set.singleton_nonempty` `IsCompact.measure_lt_top` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `isCompact_singleton` `MeasureTheory.Measure.Regular.innerRegular` `inducedMeasure_regular` `exists_continuousMap_one_of_isCompact_subset_isOpen` `instR1Space` `IsTopologicalAddGroup.regularSpace` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `lt_of_lt_of_le` `RealRMK.rieszMeasure_le_of_eq_one` `integrate_mono` `Mathlib.Tactic.Push.not_exists` `not_lt` `eq_top_or_lt_top` `ENNReal.top_mul` `LT.lt.ne'` `le_top` `ENNReal.ofReal_le_iff_le_toReal` `LT.lt.ne` `ENNReal.mul_lt_top` `ENNReal.toReal_mul` `MeasureTheory.Measure.real_def` `smul_eq_mul` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `CompactlySupportedContinuousMap.integrable` `BorelSpace.opensMeasurable` `MeasureTheory.integrable_const` `Mathlib.Tactic.Contrapose.contrapose₃` `IsOpenQuotientMap.surjective` `isOpenQuotientMap` `pushforward_apply_apply` `pullback_def` `MeasureTheory.setIntegral_support` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Topology.IsEmbedding.injective` `Topology.IsClosedEmbedding.toIsEmbedding` `isClosedEmbedding` `subset_tsupport` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Function.Exact.apply_apply_eq_zero` `exact` `add_zero` `Set.Subsingleton.eq_empty_or_singleton` `MeasureTheory.Measure.restrict_empty` `MeasureTheory.integral_zero_measure` `ENNReal.toReal_nonneg` `MeasureTheory.integral_singleton` `OpensMeasurableSpace.toMeasurableSingletonClass` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `TopologicalSpace.DiscreteTopology.metrizableSpace` `MeasureTheory.Measure.addHaar_singleton` `mul_le_iff_le_one_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `ENNReal.toReal_pos`
`inducedMeasure_regular` 📖	mathematical	`TopologicalAddGroup.IsSES`	`MeasureTheory.Measure.Regular` `inducedMeasure`	—	`RealRMK.regular_rieszMeasure` `integrate_mono`
`integral_inducedMeasure` 📖	mathematical	`TopologicalAddGroup.IsSES`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `inducedMeasure` `DFunLike.coe` `CompactlySupportedContinuousMap` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `integrate`	—	`RealRMK.integral_rieszMeasure` `integrate_mono`
`integral_pullback_invFun_apply` 📖	mathematical	`TopologicalAddGroup.IsSES`	`MeasureTheory.integral` `DFunLike.coe` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instFunLike` `pullback` `Function.invFun` `Zero.instNonempty` `AddGroup.toSubtractionMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	—	`Zero.instNonempty` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `map_neg` `Function.apply_invFun_apply` `neg_add_cancel` `Function.Exact.addMonoidHom_ker_eq` `exact` `AddMonoidHom.mem_ker` `MeasureTheory.integral_add_left_eq_self` `ContinuousAdd.measurableAdd` `instSeparatelyContinuousAddOfContinuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `pullback_def` `add_assoc` `add_neg_cancel_left`
`integrate_apply` 📖	mathematical	`TopologicalAddGroup.IsSES`	`DFunLike.coe` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `integrate` `MeasureTheory.integral` `CompactlySupportedContinuousMap.instFunLike` `pushforward`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`integrate_mono` 📖	mathematical	`TopologicalAddGroup.IsSES` `CompactlySupportedContinuousMap` `Real` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder`	`Real` `Real.instLE` `DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.normedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `integrate`	—	`MeasureTheory.integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `CompactlySupportedContinuousMap.integrable` `BorelSpace.opensMeasurable` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `pushforward_mono`
`isAddHaarMeasure_inducedMeasure` 📖	mathematical	`TopologicalAddGroup.IsSES`	`MeasureTheory.Measure.IsAddHaarMeasure` `inducedMeasure`	—	`exists_continuousMap_one_of_isCompact_subset_isOpen` `instR1Space` `IsTopologicalAddGroup.regularSpace` `isOpen_univ` `Set.subset_univ` `lt_of_le_of_lt` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `integrate_mono` `RealRMK.rieszMeasure_le_of_eq_one` `ENNReal.ofReal_lt_top` `MeasureTheory.Measure.Regular.map` `inducedMeasure_regular` `instSeparatelyContinuousAddOfContinuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported` `MeasureTheory.integral_map` `AEMeasurable.const_add` `ContinuousAdd.measurableAdd` `aemeasurable_id` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `ContinuousMapClass.map_continuous` `CompactlySupportedContinuousMapClass.toContinuousMapClass` `CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `integral_inducedMeasure` `MeasureTheory.integral_add_left_eq_self` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `IsOpenQuotientMap.surjective` `isOpenQuotientMap` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `pushforward_apply_apply` `pullback_def` `add_assoc` `add_neg_cancel_left` `exists_compact_subset` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `pushforward_mono` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `inducedMeasure.eq_1` `lt_imp_lt_of_le_of_le` `le_refl` `RealRMK.le_rieszMeasure_tsupport_subset` `ENNReal.ofReal_pos` `Zero.instNonempty` `Function.Exact.addMonoidHom_ker_eq` `exact` `AddMonoidHom.mem_ker` `Function.apply_invFun_apply` `neg_add_cancel` `interior_subset` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `ContinuousMap.continuous` `CompactlySupportedContinuousMap.hasCompactSupport` `LT.lt.ne'`
`pullback_def` 📖	mathematical	`TopologicalAddGroup.IsSES`	`DFunLike.coe` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instFunLike` `pullback` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom` `AddMonoidHom.instFunLike`	—	`CompactlySupportedContinuousMap.pullback_addMonoidHom_def` `instR1Space` `IsTopologicalAddGroup.regularSpace` `IsTopologicalAddGroup.toContinuousAdd` `isClosedEmbedding`
`pushforward_apply_apply` 📖	mathematical	`TopologicalAddGroup.IsSES`	`DFunLike.coe` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instFunLike` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `pushforward` `AddMonoidHom` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `MeasureTheory.integral` `pullback`	—	`integral_pullback_invFun_apply`
`pushforward_def` 📖	mathematical	`TopologicalAddGroup.IsSES`	`DFunLike.coe` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instFunLike` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `pushforward` `MeasureTheory.integral` `pullback` `Function.invFun` `Zero.instNonempty` `AddGroup.toSubtractionMonoid` `AddMonoidHom` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`pushforward_mono` 📖	mathematical	`TopologicalAddGroup.IsSES` `CompactlySupportedContinuousMap` `Real` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder`	`CompactlySupportedContinuousMap` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.normedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Preorder.toLE` `PartialOrder.toPreorder` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder` `DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `pushforward`	—	`MeasureTheory.integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `CompactlySupportedContinuousMap.integrable` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts`

TopologicalGroup.IsSES

Definitions

Name	Category	Theorems
`inducedMeasure` 📖	CompOp	4 math math: `inducedMeasure_regular`, `integral_inducedMeasure`, `isHaarMeasure_inducedMeasure`, `inducedMeasure_lt_of_injOn`
`integrate` 📖	CompOp	3 math math: `integral_inducedMeasure`, `integrate_apply`, `integrate_mono`
`pullback` 📖	CompOp	4 math math: `integral_pullback_invFun_apply`, `pullback_def`, `pushforward_def`, `pushforward_apply_apply`
`pushforward` 📖	CompOp	4 math math: `pushforward_def`, `integrate_apply`, `pushforward_apply_apply`, `pushforward_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inducedMeasure_lt_of_injOn` 📖	mathematical	`TopologicalGroup.IsSES` `IsOpen` `Set.InjOn` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `inducedMeasure` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Set.univ` `Set.instSingletonSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `IsOpen.measure_pos` `MeasureTheory.Measure.IsHaarMeasure.toIsOpenPosMeasure` `isOpen_discrete` `Set.singleton_nonempty` `IsCompact.measure_lt_top` `MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts` `isCompact_singleton` `MeasureTheory.Measure.Regular.innerRegular` `inducedMeasure_regular` `exists_continuousMap_one_of_isCompact_subset_isOpen` `instR1Space` `IsTopologicalGroup.regularSpace` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `lt_of_lt_of_le` `RealRMK.rieszMeasure_le_of_eq_one` `integrate_mono` `eq_top_or_lt_top` `ENNReal.top_mul` `LT.lt.ne'` `ENNReal.ofReal_le_iff_le_toReal` `LT.lt.ne` `ENNReal.mul_lt_top` `ENNReal.toReal_mul` `MeasureTheory.Measure.real_def` `smul_eq_mul` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `CompactlySupportedContinuousMap.integrable` `BorelSpace.opensMeasurable` `MeasureTheory.integrable_const` `Mathlib.Tactic.Contrapose.contrapose₃` `IsOpenQuotientMap.surjective` `isOpenQuotientMap` `pushforward_apply_apply` `pullback_def` `MeasureTheory.setIntegral_support` `LeftCancelSemigroup.toIsLeftCancelMul` `Topology.IsEmbedding.injective` `Topology.IsClosedEmbedding.toIsEmbedding` `isClosedEmbedding` `subset_tsupport` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Function.MulExact.apply_apply_eq_one` `mulExact` `mul_one` `Set.Subsingleton.eq_empty_or_singleton` `MeasureTheory.Measure.restrict_empty` `MeasureTheory.integral_zero_measure` `MeasureTheory.integral_singleton` `OpensMeasurableSpace.toMeasurableSingletonClass` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `TopologicalSpace.DiscreteTopology.metrizableSpace` `MeasureTheory.Measure.haar_singleton` `IsTopologicalGroup.toContinuousMul` `mul_le_iff_le_one_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `ENNReal.toReal_pos`
`inducedMeasure_regular` 📖	mathematical	`TopologicalGroup.IsSES`	`MeasureTheory.Measure.Regular` `inducedMeasure`	—	`RealRMK.regular_rieszMeasure` `integrate_mono`
`integral_inducedMeasure` 📖	mathematical	`TopologicalGroup.IsSES`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `inducedMeasure` `DFunLike.coe` `CompactlySupportedContinuousMap` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `integrate`	—	`RealRMK.integral_rieszMeasure` `integrate_mono`
`integral_pullback_invFun_apply` 📖	mathematical	`TopologicalGroup.IsSES`	`MeasureTheory.integral` `DFunLike.coe` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instFunLike` `pullback` `Function.invFun` `One.instNonempty` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	`One.instNonempty` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `map_inv` `Function.apply_invFun_apply` `inv_mul_cancel` `Function.MulExact.monoidHom_ker_eq` `mulExact` `MonoidHom.mem_ker` `MeasureTheory.integral_mul_left_eq_self` `ContinuousMul.measurableMul` `instSeparatelyContinuousMulOfContinuousMul` `IsTopologicalGroup.toContinuousMul` `MeasureTheory.Measure.IsHaarMeasure.toIsMulLeftInvariant` `pullback_def` `mul_assoc` `mul_inv_cancel_left`
`integrate_apply` 📖	mathematical	`TopologicalGroup.IsSES`	`DFunLike.coe` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `integrate` `MeasureTheory.integral` `CompactlySupportedContinuousMap.instFunLike` `pushforward`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`integrate_mono` 📖	mathematical	`TopologicalGroup.IsSES` `CompactlySupportedContinuousMap` `Real` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder`	`Real` `Real.instLE` `DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.normedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `integrate`	—	`MeasureTheory.integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `CompactlySupportedContinuousMap.integrable` `BorelSpace.opensMeasurable` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts` `pushforward_mono`
`isHaarMeasure_inducedMeasure` 📖	mathematical	`TopologicalGroup.IsSES`	`MeasureTheory.Measure.IsHaarMeasure` `inducedMeasure`	—	`exists_continuousMap_one_of_isCompact_subset_isOpen` `instR1Space` `IsTopologicalGroup.regularSpace` `isOpen_univ` `Set.subset_univ` `lt_of_le_of_lt` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `integrate_mono` `RealRMK.rieszMeasure_le_of_eq_one` `ENNReal.ofReal_lt_top` `MeasureTheory.Measure.Regular.map` `inducedMeasure_regular` `instSeparatelyContinuousMulOfContinuousMul` `IsTopologicalGroup.toContinuousMul` `MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported` `MeasureTheory.integral_map` `AEMeasurable.const_mul` `ContinuousMul.measurableMul` `aemeasurable_id` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `ContinuousMapClass.map_continuous` `CompactlySupportedContinuousMapClass.toContinuousMapClass` `CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `integral_inducedMeasure` `MeasureTheory.integral_mul_left_eq_self` `MeasureTheory.Measure.IsHaarMeasure.toIsMulLeftInvariant` `IsOpenQuotientMap.surjective` `isOpenQuotientMap` `map_inv` `MonoidHom.instMonoidHomClass` `map_mul` `MonoidHomClass.toMulHomClass` `pushforward_apply_apply` `pullback_def` `mul_assoc` `mul_inv_cancel_left` `exists_compact_subset` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `pushforward_mono` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `inducedMeasure.eq_1` `lt_imp_lt_of_le_of_le` `le_refl` `RealRMK.le_rieszMeasure_tsupport_subset` `ENNReal.ofReal_pos` `One.instNonempty` `Function.MulExact.monoidHom_ker_eq` `mulExact` `Function.apply_invFun_apply` `inv_mul_cancel` `interior_subset` `NeZero.charZero_one` `RCLike.charZero_rclike` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `MeasureTheory.Measure.IsHaarMeasure.toIsOpenPosMeasure` `MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts` `ContinuousMap.continuous` `CompactlySupportedContinuousMap.hasCompactSupport` `LT.lt.ne'`
`pullback_def` 📖	mathematical	`TopologicalGroup.IsSES`	`DFunLike.coe` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instFunLike` `pullback` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom` `MonoidHom.instFunLike`	—	`CompactlySupportedContinuousMap.pullback_monoidHom_def` `instR1Space` `IsTopologicalGroup.regularSpace` `IsTopologicalGroup.toContinuousMul` `isClosedEmbedding`
`pushforward_apply_apply` 📖	mathematical	`TopologicalGroup.IsSES`	`DFunLike.coe` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instFunLike` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `pushforward` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `MeasureTheory.integral` `pullback`	—	`integral_pullback_invFun_apply`
`pushforward_def` 📖	mathematical	`TopologicalGroup.IsSES`	`DFunLike.coe` `CompactlySupportedContinuousMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `CompactlySupportedContinuousMap.instFunLike` `LinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `pushforward` `MeasureTheory.integral` `pullback` `Function.invFun` `One.instNonempty` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`pushforward_mono` 📖	mathematical	`TopologicalGroup.IsSES` `CompactlySupportedContinuousMap` `Real` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder`	`CompactlySupportedContinuousMap` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.normedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Preorder.toLE` `PartialOrder.toPreorder` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder` `DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NormedSpace.toIsBoundedSMul` `LinearMap.instFunLike` `pushforward`	—	`MeasureTheory.integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `CompactlySupportedContinuousMap.integrable` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts`

---

← Back to Index