Documentation Verification Report

Basic

📁 Source: Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean

Statistics

Metric	Count
Definitions `rieszMeasure`, `rieszContent`, `rieszContentAux`	3
Theorems `monotone_of_nnreal`, `le_rieszMeasure_of_isCompact_tsupport_subset`, `le_rieszMeasure_of_tsupport_subset`, `contentRegular_rieszContent`, `exists_continuous_add_one_of_isCompact_nnreal`, `exists_lt_rieszContentAux_add_pos`, `rieszContentAux_image_nonempty`, `rieszContentAux_le`, `rieszContentAux_mono`, `rieszContentAux_sup_le`, `rieszContentAux_union`, `rieszContent_ne_top`	12
Total	15

CompactlySupportedContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monotone_of_nnreal` 📖	mathematical	—	`Monotone` `CompactlySupportedContinuousMap` `NNReal` `instZeroNNReal` `NNReal.instTopologicalSpace` `PartialOrder.toPreorder` `partialOrder` `instPartialOrderNNReal` `DFunLike.coe` `LinearMap` `instSemiringNNReal` `RingHom.id` `Semiring.toNonAssocSemiring` `instAddCommMonoidOfContinuousAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `instModuleOfContinuousConstSMul` `Semiring.toModule` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `LinearMap.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `exists_add_of_le` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `NNReal.addLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `NNReal.instCanonicallyOrderedAdd`

NNRealRMK

Definitions

Name	Category	Theorems
`rieszMeasure` 📖	CompOp	7 math math: `lintegral_rieszMeasure`, `integralLinearMap_rieszMeasure`, `le_rieszMeasure_of_isCompact_tsupport_subset`, `le_rieszMeasure_of_tsupport_subset`, `rieszMeasure_regular`, `integral_rieszMeasure`, `rieszMeasure_integralLinearMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_rieszMeasure_of_isCompact_tsupport_subset` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `CompactlySupportedContinuousMap` `instZeroNNReal` `NNReal.instTopologicalSpace` `CompactlySupportedContinuousMap.instFunLike` `instOneNNReal` `IsCompact` `Set` `Set.instHasSubset` `tsupport`	`ENNReal` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `LinearMap` `instSemiringNNReal` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `Semiring.toModule` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `LinearMap.instFunLike` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `rieszMeasure`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `MeasureTheory.Content.measure_eq_content_of_regular` `T2Space.r1Space` `contentRegular_rieszContent` `le_iff_forall_pos_le_add` `NNReal.instDenselyOrdered` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNReal.instCanonicallyOrderedAdd` `NNReal.addLeftReflectLT` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `exists_lt_rieszContentAux_add_pos` `le_trans` `CompactlySupportedContinuousMap.monotone_of_nnreal` `Set.mem_of_subset_of_mem` `image_eq_zero_of_notMem_tsupport` `zero_le` `LT.lt.le`
`le_rieszMeasure_of_tsupport_subset` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `CompactlySupportedContinuousMap` `instZeroNNReal` `NNReal.instTopologicalSpace` `CompactlySupportedContinuousMap.instFunLike` `instOneNNReal` `Set` `Set.instHasSubset` `tsupport`	`ENNReal` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `LinearMap` `instSemiringNNReal` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `Semiring.toModule` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `LinearMap.instFunLike` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `rieszMeasure`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `le_trans` `le_rieszMeasure_of_isCompact_tsupport_subset` `CompactlySupportedContinuousMap.hasCompactSupport` `subset_rfl` `Set.instReflSubset` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`

(root)

Definitions

Name	Category	Theorems
`rieszContent` 📖	CompOp	1 math math: `contentRegular_rieszContent`
`rieszContentAux` 📖	CompOp	5 math math: `rieszContentAux_sup_le`, `rieszContentAux_mono`, `exists_lt_rieszContentAux_add_pos`, `rieszContentAux_union`, `rieszContentAux_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contentRegular_rieszContent` 📖	mathematical	—	`MeasureTheory.Content.ContentRegular` `rieszContent`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `iInf_congr_Prop` `rieszContentAux_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `interior_subset` `iInf_le_iff` `rieszContentAux.eq_1` `ENNReal.le_coe_iff` `exists_compact_superset` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `TopologicalSpace.Compacts.isCompact'` `LE.le.trans_lt` `le_iInf_iff` `ENNReal.coe_lt_top` `ENNReal.coe_toNNReal` `LT.lt.ne` `NNReal.coe_le_coe` `le_iff_forall_pos_le_add` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `exists_lt_rieszContentAux_add_pos` `Real.toNNReal_pos` `LE.le.trans` `le_iff_forall_one_lt_le_mul₀` `NNReal.instIsStrictOrderedRing` `zero_le` `NNReal.instCanonicallyOrderedAdd` `mul_comm` `smul_eq_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `subset_interior_iff` `IsOpen.preimage` `ContinuousMap.continuous_toFun` `isOpen_Ioi` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `NNReal.instOrderTopology` `LT.lt.trans_le` `inv_lt_one_of_one_lt₀` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `Set.preimage_mono` `Set.Ioi_subset_Ici_self` `IsCompact.of_isClosed_subset` `CompactlySupportedContinuousMap.hasCompactSupport'` `IsClosed.preimage` `isClosed_Ici` `instClosedIciTopology` `subset_closure` `LT.lt.ne'` `inv_pos_of_pos` `LT.lt.trans` `zero_lt_one` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `ENNReal.toNNReal_mono` `csInf_le'` `inv_le_iff_one_le_mul₀'` `NNReal.coe_lt_coe` `Real.toNNReal_of_nonneg`
`exists_continuous_add_one_of_isCompact_nnreal` 📖	mathematical	`IsCompact` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instHasSubset` `Set.instUnion`	`Set.EqOn` `NNReal` `DFunLike.coe` `CompactlySupportedContinuousMap` `instZeroNNReal` `NNReal.instTopologicalSpace` `CompactlySupportedContinuousMap.instFunLike` `Pi.instOne` `instOneNNReal` `CompactlySupportedContinuousMap.instAddOfContinuousAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NNReal.instIsTopologicalSemiring`	—	`Fintype.complete` `IsCompact.isClosed` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `Set.mem_iUnion` `Set.mem_union` `Set.compl_subset_iff_union` `compl_compl` `Set.subset_compl_iff_disjoint_right` `Set.mem_univ` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `exists_continuous_sum_one_of_isOpen_isCompact` `Finset.sum_apply` `Fin.sum_univ_two` `Function.notMem_support` `subset_trans` `Set.instIsTransSubset` `Set.instReflSubset` `Set.compl_subset_compl` `Set.notMem_of_mem_compl` `Set.mem_of_subset_of_mem` `Set.compl_subset_compl_of_subset` `subset_closure` `Set.union_subset_iff` `AddZeroClass.zero_add` `AddMonoid.add_zero` `Real.toNNReal_add_toNNReal` `add_comm`
`exists_lt_rieszContentAux_add_pos` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`Preorder.toLE` `instOneNNReal` `DFunLike.coe` `CompactlySupportedContinuousMap` `NNReal.instTopologicalSpace` `CompactlySupportedContinuousMap.instFunLike` `LinearMap` `instSemiringNNReal` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `Semiring.toModule` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `LinearMap.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `rieszContentAux`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `exists_lt_of_csInf_lt` `rieszContentAux_image_nonempty` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono`
`rieszContentAux_image_nonempty` 📖	mathematical	—	`Set.Nonempty` `NNReal` `Set.image` `CompactlySupportedContinuousMap` `instZeroNNReal` `NNReal.instTopologicalSpace` `DFunLike.coe` `LinearMap` `instSemiringNNReal` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `Semiring.toModule` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `LinearMap.instFunLike` `setOf`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `Set.image_nonempty` `exists_compact_superset` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `TopologicalSpace.Compacts.isCompact'` `IsCompact.of_isClosed_subset` `isClosed_closure` `closure_eq_iff_isClosed` `IsCompact.isClosed` `closure_mono` `interior_subset` `exists_tsupport_one_of_isOpen_isClosed` `T2Space.r1Space` `isOpen_interior` `isClosed_tsupport` `Set.Subset.trans` `le_of_eq` `Real.toNNReal_one` `Real.toNNReal_eq_toNNReal_iff` `zero_le_one'` `Real.instZeroLEOneClass` `Set.EqOn.symm`
`rieszContentAux_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `DFunLike.coe` `CompactlySupportedContinuousMap` `instZeroNNReal` `NNReal.instTopologicalSpace` `CompactlySupportedContinuousMap.instFunLike`	`rieszContentAux` `LinearMap` `instSemiringNNReal` `RingHom.id` `Semiring.toNonAssocSemiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `Semiring.toModule` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `LinearMap.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `csInf_le` `OrderBot.bddBelow`
`rieszContentAux_mono` 📖	mathematical	`TopologicalSpace.Compacts` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Compacts.instPartialOrder`	`NNReal` `instPartialOrderNNReal` `rieszContentAux`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `csInf_le_csInf'` `rieszContentAux_image_nonempty` `Set.image_mono` `Set.setOf_subset_setOf_of_imp` `Mathlib.Tactic.GCongr.imp_trans` `mem_of_le_of_mem` `instIsConcreteLE`
`rieszContentAux_sup_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `rieszContentAux` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instMax` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `le_of_forall_pos_le_add` `NNReal.instDenselyOrdered` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNReal.instCanonicallyOrderedAdd` `NNReal.addLeftReflectLT` `Nat.instAtLeastTwoHAddOfNat` `exists_lt_rieszContentAux_add_pos` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `NNReal.instIsStrictOrderedRing` `le_add_right` `le_add_left` `LE.le.trans` `rieszContentAux_le` `le_of_lt` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `lt_of_lt_of_le` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `le_of_eq` `add_assoc` `add_comm` `add_halves` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero`
`rieszContentAux_union` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike`	`rieszContentAux` `TopologicalSpace.Compacts.instMax` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `le_antisymm` `rieszContentAux_sup_le` `le_csInf` `rieszContentAux_image_nonempty` `Function.mem_support` `ne_of_gt` `lt_of_lt_of_le` `zero_lt_one'` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `subset_trans` `Set.instIsTransSubset` `subset_closure` `exists_continuous_add_one_of_isCompact_nnreal` `TopologicalSpace.Compacts.isCompact'` `HasCompactSupport.isCompact` `CompactlySupportedContinuousMap.hasCompactSupport'` `IsTopologicalSemiring.toContinuousMul` `CompactlySupportedContinuousMap.ext` `NNReal.eq` `RightDistribClass.right_distrib` `Distrib.rightDistribClass` `MulZeroClass.mul_zero` `Set.mem_of_subset_of_mem` `one_mul` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `Set.mem_union_left` `Set.mem_union_right` `add_le_add` `NNReal.addLeftMono` `covariant_swap_add_of_covariant_add` `rieszContentAux_le`
`rieszContent_ne_top` 📖	—	—	—	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul`

---

← Back to Index