Documentation Verification Report

NormedSpace

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

Statistics

Metric	Count
Definitions `NormedSpace`	1
Theorems `exists_nhds_isBounded`, `comp_div`, `comp_mul_left'`, `comp_mul_right'`, `comp_smul`, `continuous_of_measurable`, `isAddHaarMeasure`, `integral_comp_div`, `integral_comp_inv_mul_left`, `integral_comp_inv_mul_right`, `integral_comp_inv_smul`, `integral_comp_inv_smul_of_nonneg`, `integral_comp_mul_left`, `integral_comp_mul_right`, `integral_comp_smul`, `integral_comp_smul_of_nonneg`, `setIntegral_comp_smul`, `setIntegral_comp_smul_of_pos`, `integrable_comp`, `integrable_comp_div_iff`, `integrable_comp_mul_left_iff`, `integrable_comp_mul_right_iff`, `integrable_comp_smul_iff`, `integral_comp`, `exists_nhds_isBounded`	25
Total	26

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nhds_isBounded` 📖	mathematical	`Measurable` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `instFunLike`	`Set` `Filter` `Filter.instMembership` `nhds` `Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddGroup.toPseudoMetricSpace` `Set.image`	—	`TopologicalSpace.PositiveCompacts.nonempty'` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `Zero.instNonempty` `Eq.not_gt` `Set.inter_univ` `Metric.iUnion_ball_nat` `Set.preimage_iUnion` `Set.inter_iUnion` `MeasureTheory.measure_iUnion_null_iff` `MeasureTheory.Measure.instOuterMeasureClass` `instCountableNat` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `Mathlib.Tactic.Push.not_exists` `not_lt` `IsOpen.measure_pos` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure` `isOpen_interior` `TopologicalSpace.PositiveCompacts.interior_nonempty` `zero_add` `op_vadd_eq_add` `vadd_mem_nhds_vadd` `VAddCommClass.continuousConstVAdd` `AddSemigroup.opposite_vaddCommClass` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos_ne_top` `MeasureTheory.Measure.Regular.instInnerRegularCompactLTTop` `MeasureTheory.Measure.regular_addHaarMeasure` `MeasurableSet.inter` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `measurableSet_ball` `MeasureTheory.measure_mono_top` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `interior_subset` `IsCompact.measure_ne_top` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `TopologicalSpace.PositiveCompacts.isCompact` `Bornology.IsBounded.subset` `Metric.isBounded_ball` `Set.image_mono` `Set.inter_subset_right` `Set.image_preimage_subset` `Set.image_op_vadd_distrib` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `Set.image_sub` `Bornology.IsBounded.vadd` `NormedAddGroup.to_isIsometricVAdd_right` `Bornology.IsBounded.sub`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable_comp` 📖	mathematical	—	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `MeasureSpace.volume`	—	`RingHomInvPair.ids` `MeasurePreserving.integrable_comp_emb` `LinearIsometryEquiv.measurePreserving` `MeasurableEquiv.measurableEmbedding`
`integrable_comp_div_iff` 📖	mathematical	—	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureSpace.toMeasurableSpace` `Real.measureSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `MeasureSpace.volume`	—	`integrable_comp_mul_right_iff` `inv_ne_zero`
`integrable_comp_mul_left_iff` 📖	mathematical	—	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Real.instMul` `MeasureSpace.volume`	—	`integrable_comp_smul_iff` `Real.borelSpace` `FiniteDimensional.rclike_to_real` `instIsAddHaarMeasureVolume`
`integrable_comp_mul_right_iff` 📖	mathematical	—	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Real.instMul` `MeasureSpace.volume`	—	`mul_comm` `integrable_comp_mul_left_iff`
`integrable_comp_smul_iff` 📖	mathematical	—	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`Units.continuousConstSMul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isUnit_iff_ne_zero` `integrable_map_equiv` `IsScalarTower.right` `Measure.map_addHaar_smul` `integrable_smul_measure` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_ne_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `ENNReal.ofReal_ne_top` `SemigroupAction.mul_smul` `mul_inv_cancel₀` `one_smul`
`integral_comp` 📖	mathematical	—	`integral` `MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureSpace.volume` `DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike`	—	`RingHomInvPair.ids` `MeasurePreserving.integral_comp'` `LinearIsometryEquiv.measurePreserving`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_div` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`MeasureTheory.integrable_comp_div_iff`
`comp_mul_left'` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume`	`Real.instMul`	—	`MeasureTheory.integrable_comp_mul_left_iff`
`comp_mul_right'` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume`	`Real.instMul`	—	`MeasureTheory.integrable_comp_mul_right_iff`
`comp_smul` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`MeasureTheory.integrable_comp_smul_iff`

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_comp_div` 📖	mathematical	—	`MeasureTheory.integral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `abs` `Real.lattice` `Real.instAddGroup`	—	`integral_comp_inv_mul_right`
`integral_comp_inv_mul_left` 📖	mathematical	—	`MeasureTheory.integral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `Real.instMul` `Real.instInv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `abs` `Real.lattice` `Real.instAddGroup`	—	`integral_comp_inv_smul` `Real.borelSpace` `FiniteDimensional.rclike_to_real` `instIsAddHaarMeasureVolume` `Module.finrank_self` `commRing_strongRankCondition` `Real.instNontrivial` `pow_one`
`integral_comp_inv_mul_right` 📖	mathematical	—	`MeasureTheory.integral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `Real.instMul` `Real.instInv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `abs` `Real.lattice` `Real.instAddGroup`	—	`mul_comm` `integral_comp_inv_mul_left`
`integral_comp_inv_smul` 📖	mathematical	—	`MeasureTheory.integral` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `abs` `Real.lattice` `Real.instAddGroup` `Monoid.toNatPow` `Module.finrank`	—	`integral_comp_smul` `inv_pow` `inv_inv`
`integral_comp_inv_smul_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`MeasureTheory.integral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Monoid.toNatPow` `Module.finrank`	—	`integral_comp_inv_smul` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`integral_comp_mul_left` 📖	mathematical	—	`MeasureTheory.integral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `Real.instMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `abs` `Real.lattice` `Real.instAddGroup` `Real.instInv`	—	`integral_comp_smul` `Real.borelSpace` `FiniteDimensional.rclike_to_real` `instIsAddHaarMeasureVolume` `Module.finrank_self` `commRing_strongRankCondition` `Real.instNontrivial` `pow_one`
`integral_comp_mul_right` 📖	mathematical	—	`MeasureTheory.integral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `Real.instMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `abs` `Real.lattice` `Real.instAddGroup` `Real.instInv`	—	`mul_comm` `integral_comp_mul_left`
`integral_comp_smul` 📖	mathematical	—	`MeasureTheory.integral` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `abs` `Real.lattice` `Real.instAddGroup` `Real.instInv` `Monoid.toNatPow` `Module.finrank`	—	`eq_or_ne` `zero_smul` `MeasureTheory.integral_const` `Module.finrank_zero_iff` `commRing_strongRankCondition` `Real.instNontrivial` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `pow_zero` `inv_one` `abs_one` `Real.instIsOrderedRing` `one_smul` `Module.finrank_pos_iff` `MeasureTheory.measure_univ_of_isAddLeftInvariant` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `RealNormedSpace.noncompactSpace` `IsAddHaarMeasure.toIsOpenPosMeasure` `IsAddHaarMeasure.toIsAddLeftInvariant` `zero_pow` `LT.lt.ne'` `inv_zero` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Units.continuousConstSMul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isUnit_iff_ne_zero` `MeasureTheory.integral_map_equiv` `IsScalarTower.right` `map_addHaar_smul` `MeasureTheory.integral_smul_measure` `ENNReal.toReal_ofReal` `covariant_swap_add_of_covariant_add` `MeasureTheory.integral_def` `abs_inv` `Real.instIsStrictOrderedRing` `abs_pow` `smul_zero`
`integral_comp_smul_of_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`MeasureTheory.integral` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Monoid.toNatPow` `Module.finrank`	—	`integral_comp_smul` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`setIntegral_comp_smul` 📖	mathematical	—	`MeasureTheory.integral` `restrict` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `abs` `Real.lattice` `Real.instAddGroup` `Real.instInv` `Monoid.toNatPow` `Module.finrank` `Set` `Set.smulSet`	—	`Units.continuousConstSMul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `MeasurableEquiv.symm_comp_self` `MeasureTheory.setIntegral_map_equiv` `IsScalarTower.right` `map_addHaar_smul` `abs_inv` `Real.instIsStrictOrderedRing` `abs_pow` `Real.instIsOrderedRing` `restrict_smul` `MeasureTheory.integral_smul_measure` `ENNReal.toReal_ofReal` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Set.ext` `Set.mem_smul_set_iff_inv_smul_mem₀`
`setIntegral_comp_smul_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.integral` `restrict` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Monoid.toNatPow` `Module.finrank` `Set` `Set.smulSet`	—	`setIntegral_comp_smul` `LT.lt.ne'` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le`

MeasureTheory.Measure.AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_of_measurable` 📖	mathematical	`Measurable` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddMonoidHom.instFunLike`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`AddMonoidHom.exists_nhds_isBounded` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `AddMonoidHom.continuous_of_isBounded_nhds_zero`

MeasureTheory.Measure.MapLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddHaarMeasure` 📖	mathematical	—	`MeasureTheory.Measure.IsAddHaarMeasure` `AddCommGroup.toAddGroup` `MeasureTheory.Measure.map` `DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv`	—	`RingHomInvPair.ids` `ContinuousLinearEquiv.isAddHaarMeasure_map`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nhds_isBounded` 📖	mathematical	`Measurable` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SeminormedGroup.toGroup` `instFunLike`	`Set` `Filter` `Filter.instMembership` `nhds` `Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedGroup.toPseudoMetricSpace` `Set.image`	—	`TopologicalSpace.PositiveCompacts.nonempty'` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `One.instNonempty` `Eq.not_gt` `Set.inter_univ` `Metric.iUnion_ball_nat` `MeasureTheory.Measure.instOuterMeasureClass` `instCountableNat` `ENNReal.instCanonicallyOrderedAdd` `IsOpen.measure_pos` `MeasureTheory.Measure.IsHaarMeasure.toIsOpenPosMeasure` `MeasureTheory.Measure.isHaarMeasure_haarMeasure` `isOpen_interior` `TopologicalSpace.PositiveCompacts.interior_nonempty` `one_mul` `op_smul_eq_mul` `smul_mem_nhds_smul` `SMulCommClass.continuousConstSMul` `Semigroup.opposite_smulCommClass` `IsTopologicalGroup.toContinuousMul` `MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos_ne_top` `MeasureTheory.Measure.Regular.instInnerRegularCompactLTTop` `MeasureTheory.Measure.regular_haarMeasure` `MeasurableSet.inter` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `measurableSet_ball` `MeasureTheory.measure_mono_top` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `interior_subset` `IsCompact.measure_ne_top` `MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts` `TopologicalSpace.PositiveCompacts.isCompact` `Bornology.IsBounded.subset` `Metric.isBounded_ball` `Set.image_mono` `Set.inter_subset_right` `Set.image_preimage_subset` `Set.image_op_smul_distrib` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `Set.image_div` `Bornology.IsBounded.smul` `NormedGroup.to_isIsometricSMul_right` `Bornology.IsBounded.div`

(root)

Definitions

Name	Category	Theorems
`NormedSpace` 📖	CompData	4 math math: `Manifold.IsImmersionAt_def`, `PiTensorProduct.dualSeminorms_bounded`, `PiTensorProduct.injectiveSeminorm_apply`, `PiTensorProduct.injectiveSeminorm_def`

---

← Back to Index