Documentation Verification Report

BoundedOperation

📁 Source: Mathlib/Topology/Bornology/BoundedOperation.lean

Statistics

Metric	Count
Definitions `BoundedAdd`, `BoundedMul`, `BoundedSub`	3
Theorems `isBounded_add`, `isBounded_mul`, `isBounded_sub`, `lipschitzWith_sub`, `add_bounded_of_bounded_of_bounded`, `boundedSub_of_lipschitzWith_sub`, `instBoundedAddOfLipschitzAdd`, `instBoundedMul`, `instBoundedMulNNReal`, `instBoundedMulOfLipschitzMul`, `instBoundedSub`, `instBoundedSubNNReal`, `isBounded_add`, `isBounded_mul`, `isBounded_nsmul`, `isBounded_pow`, `isBounded_sub`, `mul_bounded_of_bounded_of_bounded`, `sub_bounded_of_bounded_of_bounded`, `tendsto_add_const_cobounded`, `tendsto_const_add_cobounded`, `tendsto_const_sub_cobounded`, `tendsto_sub_const_cobounded`	23
Total	26

BoundedAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBounded_add` 📖	mathematical	`Bornology.IsBounded`	`Set` `Set.add`	—	—

BoundedMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBounded_mul` 📖	mathematical	`Bornology.IsBounded`	`Set` `Set.mul`	—	—

BoundedSub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBounded_sub` 📖	mathematical	`Bornology.IsBounded`	`Set` `Set.sub`	—	—

SeminormedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lipschitzWith_sub` 📖	mathematical	—	`LipschitzWith` `Prod.pseudoEMetricSpaceMax` `PseudoMetricSpace.toPseudoEMetricSpace` `toPseudoMetricSpace` `NNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Nat.instAtLeastTwoHAddOfNat` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `toSeminormedAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_add` `Nat.cast_one` `LipschitzWith.sub` `LipschitzWith.prod_fst` `LipschitzWith.prod_snd`

(root)

Definitions

Name	Category	Theorems
`BoundedAdd` 📖	CompData	1 math math: `instBoundedAddOfLipschitzAdd`
`BoundedMul` 📖	CompData	3 math math: `instBoundedMul`, `instBoundedMulOfLipschitzMul`, `instBoundedMulNNReal`
`BoundedSub` 📖	CompData	3 math math: `boundedSub_of_lipschitzWith_sub`, `instBoundedSubNNReal`, `instBoundedSub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_bounded_of_bounded_of_bounded` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`Pi.instAdd`	—	`Metric.isBounded_iff` `isBounded_add` `Metric.isBounded_range_iff` `Set.add_mem_add` `Set.mem_range_self`
`boundedSub_of_lipschitzWith_sub` 📖	mathematical	`LipschitzWith` `Prod.pseudoEMetricSpaceMax` `PseudoMetricSpace.toPseudoEMetricSpace`	`BoundedSub` `PseudoMetricSpace.toBornology`	—	`Bornology.IsBounded.prod` `Set.image_prod` `LipschitzWith.isBounded_image`
`instBoundedAddOfLipschitzAdd` 📖	mathematical	—	`BoundedAdd` `PseudoMetricSpace.toBornology` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Bornology.IsBounded.prod` `LipschitzAdd.lipschitz_add` `Set.ext` `Set.mem_image` `Set.mem_prod` `Set.add_mem_add` `LipschitzWith.isBounded_image`
`instBoundedMul` 📖	mathematical	—	`BoundedMul` `PseudoMetricSpace.toBornology` `NonUnitalSeminormedRing.toPseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSeminormedRing.toNonUnitalRing`	—	`Metric.isBounded_iff_subset_closedBall` `Metric.isBounded_iff` `Nat.instAtLeastTwoHAddOfNat` `Set.mem_mul` `dist_eq_norm` `Metric.nonempty_closedBall` `LE.le.trans` `norm_mul_le` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `mem_closedBall_zero_iff` `norm_nonneg` `norm_sub_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mul_assoc`
`instBoundedMulNNReal` 📖	mathematical	—	`BoundedMul` `NNReal` `PseudoMetricSpace.toBornology` `instPseudoMetricSpaceNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`Metric.isBounded_iff_subset_closedBall` `IsCompact.prod` `ProperSpace.isCompact_closedBall` `NNReal.instProperSpace` `Bornology.IsBounded.subset` `IsCompact.isBounded` `IsCompact.image` `continuous_mul` `IsTopologicalSemiring.toContinuousMul` `NNReal.instIsTopologicalSemiring`
`instBoundedMulOfLipschitzMul` 📖	mathematical	—	`BoundedMul` `PseudoMetricSpace.toBornology` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Bornology.IsBounded.prod` `LipschitzMul.lipschitz_mul` `Set.ext` `Set.mul_mem_mul` `LipschitzWith.isBounded_image`
`instBoundedSub` 📖	mathematical	—	`BoundedSub` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`boundedSub_of_lipschitzWith_sub` `Nat.instAtLeastTwoHAddOfNat` `SeminormedAddCommGroup.lipschitzWith_sub`
`instBoundedSubNNReal` 📖	mathematical	—	`BoundedSub` `NNReal` `PseudoMetricSpace.toBornology` `instPseudoMetricSpaceNNReal` `NNReal.instSub`	—	`boundedSub_of_lipschitzWith_sub` `Nat.instAtLeastTwoHAddOfNat` `NNReal.lipschitzWith_sub`
`isBounded_add` 📖	mathematical	`Bornology.IsBounded`	`Set` `Set.add`	—	`BoundedAdd.isBounded_add`
`isBounded_mul` 📖	mathematical	`Bornology.IsBounded`	`Set` `Set.mul`	—	`BoundedMul.isBounded_mul`
`isBounded_nsmul` 📖	mathematical	`Bornology.IsBounded`	`Set.image` `AddMonoid.toNatSMul`	—	`Set.image_congr` `zero_nsmul` `Set.image_empty` `Bornology.isBounded_empty` `Set.Nonempty.image_const` `Set.nonempty_iff_ne_empty` `Bornology.isBounded_singleton` `Set.mem_image` `succ_nsmul` `Set.add_mem_add` `Bornology.IsBounded.subset` `isBounded_add`
`isBounded_pow` 📖	mathematical	`Bornology.IsBounded`	`Set.image` `Monoid.toNatPow`	—	`Set.image_congr` `pow_zero` `Set.image_empty` `Set.Nonempty.image_const` `pow_succ` `Set.mul_mem_mul` `Bornology.IsBounded.subset` `isBounded_mul`
`isBounded_sub` 📖	mathematical	`Bornology.IsBounded`	`Set` `Set.sub`	—	`BoundedSub.isBounded_sub`
`mul_bounded_of_bounded_of_bounded` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`Pi.instMul`	—	`Metric.isBounded_iff` `isBounded_mul` `Metric.isBounded_range_iff` `Set.mul_mem_mul` `Set.mem_range_self`
`sub_bounded_of_bounded_of_bounded` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`Pi.instSub`	—	`Metric.isBounded_iff` `isBounded_sub` `Metric.isBounded_range_iff` `Set.sub_mem_sub` `Set.mem_range_self`
`tendsto_add_const_cobounded` 📖	mathematical	—	`Filter.Tendsto` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Filter.mem_map` `Bornology.isCobounded_def` `Bornology.isBounded_compl_iff` `Set.preimage_compl` `Set.ext` `Set.sub_singleton` `isBounded_sub` `instBoundedSub` `Bornology.isBounded_singleton`
`tendsto_const_add_cobounded` 📖	mathematical	—	`Filter.Tendsto` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Filter.mem_map` `Bornology.isCobounded_def` `Bornology.isBounded_compl_iff` `Set.preimage_compl` `Set.ext` `Set.singleton_add` `Set.image_add_left` `neg_neg` `isBounded_add` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `Bornology.isBounded_singleton`
`tendsto_const_sub_cobounded` 📖	mathematical	—	`Filter.Tendsto` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`sub_eq_add_neg` `Filter.Tendsto.comp` `tendsto_const_add_cobounded` `Filter.tendsto_neg_cobounded`
`tendsto_sub_const_cobounded` 📖	mathematical	—	`Filter.Tendsto` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`sub_eq_add_neg` `tendsto_add_const_cobounded`

---

← Back to Index