Documentation Verification Report

Defs

📁 Source: Mathlib/Topology/Algebra/Monoid/Defs.lean

Statistics

Metric	Count
Definitions `ContinuousAdd`, `ContinuousMul`	2
Theorems `add`, `fun_add`, `fun_mul`, `mul`, `continuous_add`, `add`, `fun_add`, `fun_mul`, `mul`, `continuous_mul`, `add`, `fun_add`, `fun_mul`, `mul`, `add`, `fun_add`, `fun_mul`, `mul`, `add`, `mul`, `tendsto_of_div_tendsto_one`, `tendsto_of_sub_tendsto_zero`, `continuous_add`, `continuous_mul`	24
Total	26

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Continuous`	`Pi.instAdd`	—	`comp₂` `continuous_add`
`fun_add` 📖	—	`Continuous`	—	—	`add`
`fun_mul` 📖	—	`Continuous`	—	—	`mul`
`mul` 📖	mathematical	`Continuous`	`Pi.instMul`	—	`comp₂` `continuous_mul`

ContinuousAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_add` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd`	—	—

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ContinuousAt`	`Pi.instAdd`	—	`Filter.Tendsto.add`
`fun_add` 📖	—	`ContinuousAt`	—	—	`add`
`fun_mul` 📖	—	`ContinuousAt`	—	—	`mul`
`mul` 📖	mathematical	`ContinuousAt`	`Pi.instMul`	—	`Filter.Tendsto.mul`

ContinuousMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_mul` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd`	—	—

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ContinuousOn`	`Pi.instAdd`	—	`ContinuousWithinAt.add`
`fun_add` 📖	—	`ContinuousOn`	—	—	`add`
`fun_mul` 📖	—	`ContinuousOn`	—	—	`mul`
`mul` 📖	mathematical	`ContinuousOn`	`Pi.instMul`	—	`ContinuousWithinAt.mul`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`ContinuousWithinAt`	`Pi.instAdd`	—	`Filter.Tendsto.add`
`fun_add` 📖	—	`ContinuousWithinAt`	—	—	`add`
`fun_mul` 📖	—	`ContinuousWithinAt`	—	—	`mul`
`mul` 📖	mathematical	`ContinuousWithinAt`	`Pi.instMul`	—	`Filter.Tendsto.mul`

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_of_div_tendsto_one` 📖	—	`Tendsto` `nhds` `Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	—	`mul_div_cancel` `mul_one` `Tendsto.mul`
`tendsto_of_sub_tendsto_zero` 📖	—	`Tendsto` `nhds` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`add_sub_cancel` `add_zero` `Tendsto.add`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`Filter.Tendsto` `nhds`	—	—	`comp` `Continuous.tendsto` `continuous_add` `prodMk_nhds`
`mul` 📖	—	`Filter.Tendsto` `nhds`	—	—	`comp` `Continuous.tendsto` `continuous_mul` `prodMk_nhds`

(root)

Definitions

Name	Category	Theorems
`ContinuousAdd` 📖	CompData	34 math math: `IsTopologicalSemiring.toContinuousAdd`, `AddOpposite.instContinuousAdd`, `continuousAdd_inf`, `instContinuousAddOrderDual`, `continuousAdd_of_comm_of_nhds_zero`, `AddSubmonoid.continuousAdd`, `Topology.IsInducing.continuousAdd`, `AddSubsemigroup.continuousAdd`, `AddUnits.instContinuousAdd`, `ENNReal.instContinuousAdd`, `IsModuleTopology.toContinuousAdd`, `ENat.instContinuousAdd`, `instContinuousAddULift`, `instContinuousAddAdditiveOfContinuousMul`, `WeakBilin.instContinuousAdd`, `ContinuousAdd.of_nhds_zero`, `IsTopologicalAddGroup.toContinuousAdd`, `instContinuousAddMulOpposite`, `SeparationQuotient.instContinuousAdd`, `ContinuousLinearMapWOT.instContinuousAdd`, `Prod.continuousAdd`, `instContinuousAddMatrix`, `continuousAdd_induced`, `Pi.continuousAdd'`, `MeasureTheory.FiniteMeasure.instContinuousAdd`, `WithCStarModule.instContinuousAdd`, `continuousAdd_of_contMDiffAdd`, `TrivSqZeroExt.instContinuousAdd`, `continuousAdd_of_discreteTopology`, `ModuleTopology.continuousAdd`, `ContinuousMap.instContinuousAddOfLocallyCompactSpace`, `instContinuousAddForallOfIsTopologicalSemiring`, `ContinuousAdd.induced`, `LipschitzAdd.continuousAdd`
`ContinuousMul` 📖	CompData	33 math math: `continuousMul_inf`, `continuousMul_of_discreteTopology`, `CategoryTheory.PreGaloisCategory.instContinuousMulAutFunctorFintypeCat`, `Topology.IsInducing.continuousMul`, `ContinuousMul.of_nhds_one`, `Metric.unitBall.instContinuousMul`, `ContinuousMap.instContinuousMulOfLocallyCompactSpace`, `MulOpposite.instContinuousMul`, `IsTopologicalSemiring.toContinuousMul`, `Units.instContinuousMul`, `UniformSpace.Completion.instContinuousMul`, `ENat.instContinuousMul`, `continuousMul_induced`, `IsTopologicalGroup.toContinuousMul`, `TrivSqZeroExt.instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd`, `Subsemigroup.continuousMul`, `instContinuousMulMatrixOfContinuousAdd`, `continuousMul_of_comm_of_nhds_one`, `continuousMul_of_contMDiffMul`, `Metric.sphere.instContinuousMul`, `instContinuousMulAddOpposite`, `Pi.continuousMul'`, `WithZeroTopology.instContinuousMul`, `NonUnitalSeminormedRing.toContinuousMul`, `Submonoid.continuousMul`, `SeparationQuotient.instContinuousMul`, `instContinuousMulOrderDual`, `Metric.unitClosedBall.instContinuousMul`, `instContinuousMulMultiplicativeOfContinuousAdd`, `LipschitzMul.continuousMul`, `ContinuousMul.induced`, `instContinuousMulULift`, `Prod.continuousMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_add` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd`	—	`ContinuousAdd.continuous_add`
`continuous_mul` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd`	—	`ContinuousMul.continuous_mul`

---

← Back to Index