Documentation Verification Report

Constructions

📁 Source: Mathlib/Topology/Algebra/IsUniformGroup/Constructions.lean

Statistics

Metric	Count
Definitions	0
Theorems `comap`, `comap`, `isUniformAddGroup`, `isUniformGroup`, `instIsUniformAddGroup`, `instIsUniformGroup`, `instIsUniformAddGroup`, `instIsUniformGroup`, `instIsUniformAddGroupOfDiscreteUniformity`, `instIsUniformGroupOfDiscreteUniformity`, `isUniformAddGroup_iInf`, `isUniformAddGroup_inf`, `isUniformAddGroup_sInf`, `isUniformGroup_iInf`, `isUniformGroup_inf`, `isUniformGroup_sInf`	16
Total	16

IsUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	—	`IsUniformAddGroup` `UniformSpace.comap` `DFunLike.coe`	—	`IsUniformInducing.isUniformAddGroup`

IsUniformGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	—	`IsUniformGroup` `UniformSpace.comap` `DFunLike.coe`	—	`IsUniformInducing.isUniformGroup`

IsUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUniformAddGroup` 📖	mathematical	`IsUniformInducing` `DFunLike.coe`	`IsUniformAddGroup`	—	`uniformContinuous_iff` `map_sub` `UniformContinuous.comp` `uniformContinuous_sub` `UniformContinuous.prodMap` `uniformContinuous`
`isUniformGroup` 📖	mathematical	`IsUniformInducing` `DFunLike.coe`	`IsUniformGroup`	—	`uniformContinuous_iff` `map_div` `UniformContinuous.comp` `uniformContinuous_div` `UniformContinuous.prodMap` `uniformContinuous`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsUniformAddGroup` 📖	mathematical	`IsUniformAddGroup`	`uniformSpace` `addGroup`	—	`uniformSpace_eq` `isUniformAddGroup_iInf` `IsUniformAddGroup.comap` `AddMonoidHom.instAddMonoidHomClass`
`instIsUniformGroup` 📖	mathematical	`IsUniformGroup`	`uniformSpace` `group`	—	`uniformSpace_eq` `isUniformGroup_iInf` `IsUniformGroup.comap` `MonoidHom.instMonoidHomClass`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsUniformAddGroup` 📖	mathematical	—	`IsUniformAddGroup` `instUniformSpaceProd` `instAddGroup`	—	`instUniformSpaceProd.eq_1` `isUniformAddGroup_inf` `IsUniformAddGroup.comap` `AddMonoidHom.instAddMonoidHomClass`
`instIsUniformGroup` 📖	mathematical	—	`IsUniformGroup` `instUniformSpaceProd` `instGroup`	—	`instUniformSpaceProd.eq_1` `isUniformGroup_inf` `IsUniformGroup.comap` `MonoidHom.instMonoidHomClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsUniformAddGroupOfDiscreteUniformity` 📖	mathematical	—	`IsUniformAddGroup`	—	`DiscreteUniformity.uniformContinuous` `DiscreteUniformity.instProd`
`instIsUniformGroupOfDiscreteUniformity` 📖	mathematical	—	`IsUniformGroup`	—	`DiscreteUniformity.uniformContinuous` `DiscreteUniformity.instProd`
`isUniformAddGroup_iInf` 📖	mathematical	`IsUniformAddGroup`	`iInf` `UniformSpace` `instInfSetUniformSpace`	—	`sInf_range` `isUniformAddGroup_sInf` `Set.forall_mem_range`
`isUniformAddGroup_inf` 📖	mathematical	—	`IsUniformAddGroup` `UniformSpace` `instMinUniformSpace`	—	`inf_eq_iInf` `isUniformAddGroup_iInf`
`isUniformAddGroup_sInf` 📖	mathematical	`IsUniformAddGroup`	`InfSet.sInf` `UniformSpace` `instInfSetUniformSpace`	—	`uniformContinuous_sInf_rng` `uniformContinuous_sInf_dom₂` `IsUniformAddGroup.uniformContinuous_sub`
`isUniformGroup_iInf` 📖	mathematical	`IsUniformGroup`	`iInf` `UniformSpace` `instInfSetUniformSpace`	—	`sInf_range` `isUniformGroup_sInf` `Set.forall_mem_range`
`isUniformGroup_inf` 📖	mathematical	—	`IsUniformGroup` `UniformSpace` `instMinUniformSpace`	—	`inf_eq_iInf` `isUniformGroup_iInf`
`isUniformGroup_sInf` 📖	mathematical	`IsUniformGroup`	`InfSet.sInf` `UniformSpace` `instInfSetUniformSpace`	—	`uniformContinuous_sInf_rng` `uniformContinuous_sInf_dom₂` `IsUniformGroup.uniformContinuous_div`

---

← Back to Index