Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `ContinuousAdd`, `ContinuousMul`, `SeparatelyContinuousAdd`, `SeparatelyContinuousMul`	4
Theorems `add`, `add_const`, `const_add`, `const_mul`, `fun_add`, `fun_mul`, `mul`, `mul_const`, `continuous_add`, `add`, `add_const`, `const_add`, `const_mul`, `fun_add`, `fun_mul`, `mul`, `mul_const`, `continuous_mul`, `add`, `add_const`, `const_add`, `const_mul`, `fun_add`, `fun_mul`, `mul`, `mul_const`, `add`, `add_const`, `const_add`, `const_mul`, `fun_add`, `fun_mul`, `mul`, `mul_const`, `add`, `add_const`, `const_add`, `const_mul`, `mul`, `mul_const`, `tendsto_of_div_tendsto_one`, `tendsto_of_sub_tendsto_zero`, `continuous_add_const`, `continuous_const_add`, `continuous_const_mul`, `continuous_mul_const`, `continuous_add`, `continuous_add_const`, `continuous_const_add`, `continuous_const_mul`, `continuous_mul`, `continuous_mul_const`, `instSeparatelyContinuousAddOfContinuousAdd`, `instSeparatelyContinuousMulOfContinuousMul`	54
Total	58

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Continuous`	`Continuous` `Pi.instAdd`	—	`comp₂` `continuous_add`
`add_const` 📖	mathematical	`Continuous`	`Continuous`	—	`comp` `continuous_add_const`
`const_add` 📖	mathematical	`Continuous`	`Continuous`	—	`comp` `continuous_const_add`
`const_mul` 📖	mathematical	`Continuous`	`Continuous`	—	`comp` `continuous_const_mul`
`fun_add` 📖	mathematical	`Continuous`	`Continuous`	—	`add`
`fun_mul` 📖	mathematical	`Continuous`	`Continuous`	—	`mul`
`mul` 📖	mathematical	`Continuous`	`Continuous` `Pi.instMul`	—	`comp₂` `continuous_mul`
`mul_const` 📖	mathematical	`Continuous`	`Continuous`	—	`comp` `continuous_mul_const`

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`	`ContinuousAt` `Pi.instAdd`	—	`Filter.Tendsto.add`
`add_const` 📖	mathematical	`ContinuousAt`	`ContinuousAt`	—	`Filter.Tendsto.add_const`
`const_add` 📖	mathematical	`ContinuousAt`	`ContinuousAt`	—	`Filter.Tendsto.const_add`
`const_mul` 📖	mathematical	`ContinuousAt`	`ContinuousAt`	—	`Filter.Tendsto.const_mul`
`fun_add` 📖	mathematical	`ContinuousAt`	`ContinuousAt`	—	`add`
`fun_mul` 📖	mathematical	`ContinuousAt`	`ContinuousAt`	—	`mul`
`mul` 📖	mathematical	`ContinuousAt`	`ContinuousAt` `Pi.instMul`	—	`Filter.Tendsto.mul`
`mul_const` 📖	mathematical	`ContinuousAt`	`ContinuousAt`	—	`Filter.Tendsto.mul_const`

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`	`ContinuousOn` `Pi.instAdd`	—	`ContinuousWithinAt.add`
`add_const` 📖	mathematical	`ContinuousOn`	`ContinuousOn`	—	`ContinuousWithinAt.add_const`
`const_add` 📖	mathematical	`ContinuousOn`	`ContinuousOn`	—	`ContinuousWithinAt.const_add`
`const_mul` 📖	mathematical	`ContinuousOn`	`ContinuousOn`	—	`ContinuousWithinAt.const_mul`
`fun_add` 📖	mathematical	`ContinuousOn`	`ContinuousOn`	—	`add`
`fun_mul` 📖	mathematical	`ContinuousOn`	`ContinuousOn`	—	`mul`
`mul` 📖	mathematical	`ContinuousOn`	`ContinuousOn` `Pi.instMul`	—	`ContinuousWithinAt.mul`
`mul_const` 📖	mathematical	`ContinuousOn`	`ContinuousOn`	—	`ContinuousWithinAt.mul_const`

ContinuousWithinAt

Theorems

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

Filter

Theorems

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

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds`	—	`comp` `Continuous.tendsto` `continuous_add` `prodMk_nhds`
`add_const` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds`	—	`comp` `Continuous.tendsto` `continuous_add_const`
`const_add` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds`	—	`comp` `Continuous.tendsto` `continuous_const_add`
`const_mul` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds`	—	`comp` `Continuous.tendsto` `continuous_const_mul`
`mul` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds`	—	`comp` `Continuous.tendsto` `continuous_mul` `prodMk_nhds`
`mul_const` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter.Tendsto` `nhds`	—	`comp` `Continuous.tendsto` `continuous_mul_const`

SeparatelyContinuousAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_add_const` 📖	mathematical	—	`Continuous`	—	—
`continuous_const_add` 📖	mathematical	—	`Continuous`	—	—

SeparatelyContinuousMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_const_mul` 📖	mathematical	—	`Continuous`	—	—
`continuous_mul_const` 📖	mathematical	—	`Continuous`	—	—

(root)

Definitions

Name	Category	Theorems
`ContinuousAdd` 📖	CompData	40 math math: `IsTopologicalSemiring.toContinuousAdd`, `AddOpposite.instContinuousAdd`, `continuousAdd_inf`, `instContinuousAddOrderDual`, `RestrictedProduct.instContinuousAddCoePrincipal`, `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_indiscreteTopology`, `ContinuousAdd.of_nhds_zero`, `continuousAdd_iInf`, `IsTopologicalAddGroup.toContinuousAdd`, `instContinuousAddMulOpposite`, `SeparationQuotient.instContinuousAdd`, `ContinuousLinearMapWOT.instContinuousAdd`, `Prod.continuousAdd`, `instContinuousAddMatrix`, `continuousAdd_induced`, `Pi.continuousAdd'`, `MeasureTheory.FiniteMeasure.instContinuousAdd`, `continuousAdd_sInf`, `WithCStarModule.instContinuousAdd`, `continuousAdd_of_contMDiffAdd`, `TrivSqZeroExt.instContinuousAdd`, `continuousAdd_of_discreteTopology`, `ModuleTopology.continuousAdd`, `RestrictedProduct.instContinuousAddCoeCofinite`, `ContinuousMap.instContinuousAddOfLocallyCompactSpace`, `Pi.continuousAdd`, `ContinuousAdd.induced`, `IsSemitopologicalSemiring.toContinuousAdd`, `LipschitzAdd.continuousAdd`
`ContinuousMul` 📖	CompData	39 math math: `continuousMul_inf`, `continuousMul_of_discreteTopology`, `continuousMul_sInf`, `CategoryTheory.PreGaloisCategory.instContinuousMulAutFunctorFintypeCat`, `RestrictedProduct.instContinuousMulCoePrincipal`, `Topology.IsInducing.continuousMul`, `ContinuousMul.of_nhds_one`, `Metric.unitBall.instContinuousMul`, `ContinuousMap.instContinuousMulOfLocallyCompactSpace`, `MulOpposite.instContinuousMul`, `IsTopologicalSemiring.toContinuousMul`, `continuousMul_of_indiscreteTopology`, `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`, `RestrictedProduct.instContinuousMulCoeCofinite`, `instContinuousMulAddOpposite`, `Pi.continuousMul'`, `WithZeroTopology.instContinuousMul`, `NonUnitalSeminormedRing.toContinuousMul`, `Pi.continuousMul`, `continuousMul_iInf`, `Submonoid.continuousMul`, `SeparationQuotient.instContinuousMul`, `instContinuousMulOrderDual`, `Metric.unitClosedBall.instContinuousMul`, `instContinuousMulMultiplicativeOfContinuousAdd`, `LipschitzMul.continuousMul`, `ContinuousMul.induced`, `instContinuousMulULift`, `Prod.continuousMul`
`SeparatelyContinuousAdd` 📖	CompData	11 math math: `instSeparatelyContinuousAddOfContinuousAdd`, `AddOpposite.instSeparatelyContinuousAdd`, `AddSubmonoid.separatelyContinuousAdd`, `separatelyContinuousAdd_induced`, `instSeparatelyContinuousAddAdditiveOfSeparatelyContinuousMul`, `instSeparatelyContinuousAddULift`, `Pi.separatelyContinuousAdd`, `instSeparatelyContinuousAddOrderDual`, `AddSubsemigroup.separatelyContinuousAdd`, `Topology.IsInducing.separatelyContinuousAdd`, `Prod.separatelyContinuousAdd`
`SeparatelyContinuousMul` 📖	CompData	13 math math: `Topology.IsInducing.separatelyContinuousMul`, `instSeparatelyContinuousMulULift`, `MulOpposite.instSeparatelyContinuousMul`, `separatelyContinuousMul_induced`, `instSeparatelyContinuousMulOrderDual`, `Subsemigroup.separatelyContinuousMul`, `Submonoid.separatelyContinuousMul`, `instSeparatelyContinuousMulAddOpposite`, `IsSemitopologicalSemiring.toSeparatelyContinuousMul`, `Pi.separatelyContinuousMul`, `Prod.separatelyContinuousMul`, `instSeparatelyContinuousMulMultiplicativeOfSeparatelyContinuousAdd`, `instSeparatelyContinuousMulOfContinuousMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_add` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd`	—	`ContinuousAdd.continuous_add`
`continuous_add_const` 📖	mathematical	—	`Continuous`	—	`SeparatelyContinuousAdd.continuous_add_const`
`continuous_const_add` 📖	mathematical	—	`Continuous`	—	`SeparatelyContinuousAdd.continuous_const_add`
`continuous_const_mul` 📖	mathematical	—	`Continuous`	—	`SeparatelyContinuousMul.continuous_const_mul`
`continuous_mul` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd`	—	`ContinuousMul.continuous_mul`
`continuous_mul_const` 📖	mathematical	—	`Continuous`	—	`SeparatelyContinuousMul.continuous_mul_const`
`instSeparatelyContinuousAddOfContinuousAdd` 📖	mathematical	—	`SeparatelyContinuousAdd`	—	`Continuous.add` `continuous_const` `continuous_id`
`instSeparatelyContinuousMulOfContinuousMul` 📖	mathematical	—	`SeparatelyContinuousMul`	—	`Continuous.mul` `continuous_const` `continuous_id`

---

← Back to Index