Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `opUniformEquivLeft`, `opUniformEquivRight`, `opUniformEquivLeft`, `opUniformEquivRight`, `inv`, `neg`	6
Theorems `tendsto_coe_cofinite_of_discrete`, `comap_op_leftUniformSpace`, `comap_op_rightUniformSpace`, `isClosed_of_discrete`, `isUniformAddGroup`, `tendsto_coe_cofinite_of_discrete`, `add`, `add_const`, `const_add`, `const_mul`, `inv`, `mul`, `mul_const`, `neg`, `extend_Z_bilin`, `completeSpace_of_weaklyLocallyCompactSpace`, `completeSpace_of_weaklyLocallyCompactSpace`, `completeSpace_rightUniformSpace_iff_leftUniformSpace`, `tendstoLocallyUniformlyOn_iff`, `tendstoLocallyUniformly_iff`, `tendstoUniformlyOn_iff`, `tendstoUniformly_iff`, `completeSpace_rightUniformSpace_iff_leftUniformSpace`, `tendstoLocallyUniformlyOn_iff`, `tendstoLocallyUniformly_iff`, `tendstoUniformlyOn_iff`, `tendstoUniformly_iff`, `cauchy_iff_tendsto`, `cauchy_iff_tendsto_swapped`, `cauchy_map_iff_tendsto`, `cauchy_map_iff_tendsto_swapped`, `of_compactSpace`, `cauchy_iff_tendsto`, `cauchy_iff_tendsto_swapped`, `cauchy_map_iff_tendsto`, `cauchy_map_iff_tendsto_swapped`, `of_compactSpace`, `tendsto_coe_cofinite_of_discrete`, `comap_op_leftUniformSpace`, `comap_op_rightUniformSpace`, `completeSpace_left`, `completeSpace_left'`, `completeSpace_right`, `completeSpace_right'`, `completeSpace_left`, `completeSpace_left'`, `completeSpace_right`, `completeSpace_right'`, `isClosed_of_discrete`, `isUniformGroup`, `tendsto_coe_cofinite_of_discrete`, `add`, `div`, `fun_add`, `fun_div`, `fun_inv`, `fun_mul`, `fun_neg`, `fun_sub`, `inv`, `mul`, `neg`, `sub`, `add`, `div`, `fun_add`, `fun_div`, `fun_inv`, `fun_mul`, `fun_neg`, `fun_sub`, `inv`, `mul`, `neg`, `sub`, `add`, `div`, `fun_add`, `fun_div`, `fun_inv`, `fun_mul`, `fun_neg`, `fun_sub`, `inv`, `mul`, `neg`, `sub`, `add`, `div`, `fun_add`, `fun_div`, `fun_inv`, `fun_mul`, `fun_neg`, `fun_sub`, `inv`, `mul`, `neg`, `sub`, `add`, `div`, `fun_add`, `fun_div`, `fun_inv`, `fun_mul`, `fun_neg`, `fun_sub`, `inv`, `mul`, `neg`, `sub`, `add`, `div`, `fun_add`, `fun_div`, `fun_inv`, `fun_mul`, `fun_neg`, `fun_sub`, `inv`, `mul`, `neg`, `sub`, `comap_inv_leftUniformSpace`, `comap_neg_leftUniformSpace`, `isUniformEmbedding_translate_add`, `isUniformEmbedding_translate_mul`, `tendsto_div_comap_self`, `tendsto_sub_comap_self`, `topologicalAddGroup_is_uniform_of_compactSpace`, `topologicalGroup_is_uniform_of_compactSpace`, `totallyBounded_iff_subset_finite_iUnion_nhds_one`, `totallyBounded_iff_subset_finite_iUnion_nhds_zero`, `totallyBounded_inv`, `totallyBounded_neg`	135
Total	141

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_coe_cofinite_of_discrete` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `IsDiscrete` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `range`	`Filter.Tendsto` `Filter.cofinite` `Filter.cocompact`	—	`rangeRestrict_injective_iff` `Filter.Tendsto.comp` `AddSubgroup.tendsto_coe_cofinite_of_discrete` `Function.Injective.tendsto_cofinite`

AddOpposite

Definitions

Name	Category	Theorems
`opUniformEquivLeft` 📖	CompOp	—
`opUniformEquivRight` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_op_leftUniformSpace` 📖	mathematical	—	`UniformSpace.comap` `AddOpposite` `op` `IsTopologicalAddGroup.leftUniformSpace` `instAddGroup` `instTopologicalSpaceAddOpposite` `instIsTopologicalAddGroupAddOpposite` `IsTopologicalAddGroup.rightUniformSpace`	—	`UniformSpace.ext` `instIsTopologicalAddGroupAddOpposite` `Homeomorph.comap_nhds_eq` `Filter.comap_comap` `sub_eq_add_neg`
`comap_op_rightUniformSpace` 📖	mathematical	—	`UniformSpace.comap` `AddOpposite` `op` `IsTopologicalAddGroup.rightUniformSpace` `instAddGroup` `instTopologicalSpaceAddOpposite` `instIsTopologicalAddGroupAddOpposite` `IsTopologicalAddGroup.leftUniformSpace`	—	`UniformSpace.ext` `instIsTopologicalAddGroupAddOpposite` `Homeomorph.comap_nhds_eq` `Filter.comap_comap`

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_of_discrete` 📖	mathematical	—	`IsClosed` `SetLike.coe` `AddSubgroup` `instSetLike`	—	`isDiscrete_iff_discreteTopology` `nhds_inter_eq_singleton_of_mem_discrete` `zero_mem` `Filter.preimage_mem_comap` `isClosed_of_spaced_out` `T1Space.t0Space` `T2Space.t1Space` `Mathlib.Tactic.Contrapose.contrapose₄` `Set.mem_preimage` `Set.mem_inter` `sub_mem` `eq_of_sub_eq_zero`
`isUniformAddGroup` 📖	mathematical	—	`IsUniformAddGroup` `AddSubgroup` `SetLike.instMembership` `instSetLike` `instUniformSpaceSubtype` `toAddGroup`	—	`IsUniformAddGroup.comap` `AddMonoidHom.instAddMonoidHomClass`
`tendsto_coe_cofinite_of_discrete` 📖	mathematical	`IsDiscrete` `SetLike.coe` `AddSubgroup` `instSetLike`	`Filter.Tendsto` `SetLike.instMembership` `Filter.cofinite` `Filter.cocompact`	—	`IsClosed.tendsto_coe_cofinite_of_isDiscrete` `isClosed_of_discrete` `isDiscrete_iff_discreteTopology`

CauchySeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`CauchySeq`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_cauchySeq` `uniformContinuous_add` `prodMk`
`add_const` 📖	mathematical	`CauchySeq`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_cauchySeq` `UniformContinuous.add` `uniformContinuous_id` `uniformContinuous_const`
`const_add` 📖	mathematical	`CauchySeq`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_cauchySeq` `UniformContinuous.add` `uniformContinuous_const` `uniformContinuous_id`
`const_mul` 📖	mathematical	`CauchySeq`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_cauchySeq` `UniformContinuous.mul` `uniformContinuous_const` `uniformContinuous_id`
`inv` 📖	mathematical	`CauchySeq`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`UniformContinuous.comp_cauchySeq` `uniformContinuous_inv`
`mul` 📖	mathematical	`CauchySeq`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_cauchySeq` `uniformContinuous_mul` `prodMk`
`mul_const` 📖	mathematical	`CauchySeq`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_cauchySeq` `UniformContinuous.mul` `uniformContinuous_id` `uniformContinuous_const`
`neg` 📖	mathematical	`CauchySeq`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`UniformContinuous.comp_cauchySeq` `uniformContinuous_neg`

IsDenseInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend_Z_bilin` 📖	mathematical	`IsDenseInducing` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `Continuous` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `AddMonoidHom.instAddCommGroup`	`extend` `prodMap`	—	`continuous_extend_of_cauchy` `prodMap` `Filter.NeBot.map` `Filter.comap_neBot` `mem_closure_iff_nhds` `dense` `Filter.mem_comap` `Filter.mem_map` `nhds_prod_eq` `Filter.mem_prod_same_iff` `Filter.prod_mem_prod` `uniformity_eq_comap_nhds_zero` `IsUniformAddGroup.isRightUniformAddGroup` `Filter.prod_map_map_eq` `Filter.map_le_iff_le_comap` `Filter.map_map` `Filter.prod_comap_comap_eq`

IsRightUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_of_weaklyLocallyCompactSpace` 📖	mathematical	—	`CompleteSpace`	—	`WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `Filter.Eventually.exists` `Filter.Eventually.curry` `Filter.Tendsto.eventually_mem` `Filter.tendsto_iff_comap` `uniformity_eq_comap_nhds_zero` `cauchy_iff_le` `IsCompact.isComplete` `IsCompact.vadd` `VAddCommClass.continuousConstVAdd` `AddSemigroup.opposite_vaddCommClass` `IsTopologicalAddGroup.toContinuousAdd` `toIsTopologicalAddGroup` `Filter.le_principal_iff` `Filter.eventually_mem_set` `Set.mem_vadd_set_iff_neg_vadd_mem` `sub_eq_add_neg`

IsRightUniformGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_of_weaklyLocallyCompactSpace` 📖	mathematical	—	`CompleteSpace`	—	`WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `Filter.Eventually.exists` `Filter.Eventually.curry` `Filter.Tendsto.eventually_mem` `Filter.tendsto_iff_comap` `uniformity_eq_comap_nhds_one` `cauchy_iff_le` `IsCompact.isComplete` `IsCompact.smul` `SMulCommClass.continuousConstSMul` `Semigroup.opposite_smulCommClass` `IsTopologicalGroup.toContinuousMul` `toIsTopologicalGroup` `div_eq_mul_inv`

IsTopologicalAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_rightUniformSpace_iff_leftUniformSpace` 📖	mathematical	—	`CompleteSpace` `rightUniformSpace` `leftUniformSpace`	—	`UniformEquiv.completeSpace_iff`
`tendstoLocallyUniformlyOn_iff` 📖	mathematical	`rightUniformSpace` `UniformSpace.toTopologicalSpace`	`TendstoLocallyUniformlyOn` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Filter.Eventually`	—	`Filter.mem_of_superset`
`tendstoLocallyUniformly_iff` 📖	mathematical	`rightUniformSpace` `UniformSpace.toTopologicalSpace`	`TendstoLocallyUniformly` `Set` `Filter` `Filter.instMembership` `nhds` `Filter.Eventually`	—	`Filter.mem_of_superset`
`tendstoUniformlyOn_iff` 📖	mathematical	`rightUniformSpace` `UniformSpace.toTopologicalSpace`	`TendstoUniformlyOn` `Filter.Eventually`	—	`Filter.mem_of_superset`
`tendstoUniformly_iff` 📖	mathematical	`rightUniformSpace` `UniformSpace.toTopologicalSpace`	`TendstoUniformly` `Filter.Eventually`	—	`Filter.mem_of_superset`

IsTopologicalGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_rightUniformSpace_iff_leftUniformSpace` 📖	mathematical	—	`CompleteSpace` `rightUniformSpace` `leftUniformSpace`	—	`UniformEquiv.completeSpace_iff`
`tendstoLocallyUniformlyOn_iff` 📖	mathematical	`rightUniformSpace` `UniformSpace.toTopologicalSpace`	`TendstoLocallyUniformlyOn` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Filter.Eventually`	—	`Filter.mem_of_superset`
`tendstoLocallyUniformly_iff` 📖	mathematical	`rightUniformSpace` `UniformSpace.toTopologicalSpace`	`TendstoLocallyUniformly` `Set` `Filter` `Filter.instMembership` `nhds` `Filter.Eventually`	—	`Filter.mem_of_superset`
`tendstoUniformlyOn_iff` 📖	mathematical	`rightUniformSpace` `UniformSpace.toTopologicalSpace`	`TendstoUniformlyOn` `Filter.Eventually`	—	`Filter.mem_of_superset`
`tendstoUniformly_iff` 📖	mathematical	`rightUniformSpace` `UniformSpace.toTopologicalSpace`	`TendstoUniformly` `Filter.Eventually`	—	`Filter.mem_of_superset`

IsUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchy_iff_tendsto` 📖	mathematical	—	`Cauchy` `Filter.NeBot` `Filter.Tendsto` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`uniformity_eq_comap_nhds_zero_swapped` `isRightUniformAddGroup` `Filter.tendsto_iff_comap`
`cauchy_iff_tendsto_swapped` 📖	mathematical	—	`Cauchy` `Filter.NeBot` `Filter.Tendsto` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`uniformity_eq_comap_nhds_zero` `isRightUniformAddGroup` `Filter.tendsto_iff_comap`
`cauchy_map_iff_tendsto` 📖	mathematical	—	`Cauchy` `Filter.map` `Filter.NeBot` `Filter.Tendsto` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`cauchy_map_iff` `uniformity_eq_comap_nhds_zero_swapped` `isRightUniformAddGroup` `Filter.tendsto_comap_iff`
`cauchy_map_iff_tendsto_swapped` 📖	mathematical	—	`Cauchy` `Filter.map` `Filter.NeBot` `Filter.Tendsto` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`cauchy_map_iff` `uniformity_eq_comap_nhds_zero` `isRightUniformAddGroup` `Filter.tendsto_comap_iff`
`of_compactSpace` 📖	mathematical	—	`IsUniformAddGroup`	—	`CompactSpace.uniformContinuous_of_continuous` `instCompactSpaceProd` `ContinuousSub.continuous_sub`

IsUniformGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchy_iff_tendsto` 📖	mathematical	—	`Cauchy` `Filter.NeBot` `Filter.Tendsto` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`uniformity_eq_comap_nhds_one_swapped` `isRightUniformGroup`
`cauchy_iff_tendsto_swapped` 📖	mathematical	—	`Cauchy` `Filter.NeBot` `Filter.Tendsto` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`uniformity_eq_comap_nhds_one` `isRightUniformGroup`
`cauchy_map_iff_tendsto` 📖	mathematical	—	`Cauchy` `Filter.map` `Filter.NeBot` `Filter.Tendsto` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`uniformity_eq_comap_nhds_one_swapped` `isRightUniformGroup`
`cauchy_map_iff_tendsto_swapped` 📖	mathematical	—	`Cauchy` `Filter.map` `Filter.NeBot` `Filter.Tendsto` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`uniformity_eq_comap_nhds_one` `isRightUniformGroup`
`of_compactSpace` 📖	mathematical	—	`IsUniformGroup`	—	`CompactSpace.uniformContinuous_of_continuous` `instCompactSpaceProd` `ContinuousDiv.continuous_div'`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_coe_cofinite_of_discrete` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `IsDiscrete` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `range`	`Filter.Tendsto` `Filter.cofinite` `Filter.cocompact`	—	`Filter.Tendsto.comp` `Subgroup.tendsto_coe_cofinite_of_discrete` `Function.Injective.tendsto_cofinite`

MulOpposite

Definitions

Name	Category	Theorems
`opUniformEquivLeft` 📖	CompOp	—
`opUniformEquivRight` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_op_leftUniformSpace` 📖	mathematical	—	`UniformSpace.comap` `MulOpposite` `op` `IsTopologicalGroup.leftUniformSpace` `instGroup` `instTopologicalSpaceMulOpposite` `instIsTopologicalGroupMulOpposite` `IsTopologicalGroup.rightUniformSpace`	—	`UniformSpace.ext` `instIsTopologicalGroupMulOpposite` `Homeomorph.comap_nhds_eq` `Filter.comap_comap` `div_eq_mul_inv`
`comap_op_rightUniformSpace` 📖	mathematical	—	`UniformSpace.comap` `MulOpposite` `op` `IsTopologicalGroup.rightUniformSpace` `instGroup` `instTopologicalSpaceMulOpposite` `instIsTopologicalGroupMulOpposite` `IsTopologicalGroup.leftUniformSpace`	—	`UniformSpace.ext` `instIsTopologicalGroupMulOpposite` `Homeomorph.comap_nhds_eq` `Filter.comap_comap`

QuotientAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_left` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `IsTopologicalAddGroup.leftUniformSpace` `Quotient.addGroup` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `instIsTopologicalAddGroup` `IsLeftUniformAddGroup.toIsTopologicalAddGroup`	—	`IsLeftUniformAddGroup.toIsTopologicalAddGroup` `UniformSpace.ext` `IsLeftUniformAddGroup.uniformity_eq` `instIsTopologicalAddGroup` `completeSpace_left'`
`completeSpace_left'` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `IsTopologicalAddGroup.leftUniformSpace` `Quotient.addGroup` `instTopologicalSpace` `instIsTopologicalAddGroup`	—	`instIsTopologicalAddGroup` `IsTopologicalAddGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace` `completeSpace_right'`
`completeSpace_right` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `IsTopologicalAddGroup.rightUniformSpace` `Quotient.addGroup` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `instIsTopologicalAddGroup` `IsRightUniformAddGroup.toIsTopologicalAddGroup`	—	`IsRightUniformAddGroup.toIsTopologicalAddGroup` `UniformSpace.ext` `IsRightUniformAddGroup.uniformity_eq` `sub_eq_add_neg` `instIsTopologicalAddGroup` `completeSpace_right'`
`completeSpace_right'` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `IsTopologicalAddGroup.rightUniformSpace` `Quotient.addGroup` `instTopologicalSpace` `instIsTopologicalAddGroup`	—	`instIsTopologicalAddGroup` `IsTopologicalAddGroup.exists_antitone_basis_nhds_zero` `Filter.HasAntitoneBasis.map` `UniformSpace.complete_of_cauchySeq_tendsto` `Filter.comap.isCountablyGenerated` `FirstCountableTopology.nhds_generated_countable` `instFirstCountableTopology` `IsTopologicalAddGroup.toContinuousAdd` `sub_eq_add_neg` `Set.mem_image` `Filter.HasBasis.comap` `mk_zero` `nhds_eq` `forall_true_left` `Filter.HasBasis.cauchySeq_iff` `LE.le.trans_lt` `le_max_left` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `LE.le.trans` `le_max_right` `LT.lt.le` `neg_add_rev` `neg_neg` `add_neg_cancel_left` `mk_add` `mk_neg` `neg_sub` `sub_add_cancel` `mk_surjective` `le_rfl` `Filter.HasAntitoneBasis.toHasBasis` `Filter.HasBasis.cauchySeq_iff'` `sub_add_sub_cancel` `sub_self` `mem_of_mem_nhds` `Filter.HasAntitoneBasis.mem` `cauchySeq_tendsto_of_complete` `tendsto_nhds_of_cauchySeq_of_subseq` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `StrictMono.tendsto_atTop` `strictMono_nat_of_lt_succ` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_coinduced_rng`

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_left` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `IsTopologicalGroup.leftUniformSpace` `Quotient.group` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `instIsTopologicalGroup` `IsLeftUniformGroup.toIsTopologicalGroup`	—	`IsLeftUniformGroup.toIsTopologicalGroup` `UniformSpace.ext` `IsLeftUniformGroup.uniformity_eq` `instIsTopologicalGroup` `completeSpace_left'`
`completeSpace_left'` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `IsTopologicalGroup.leftUniformSpace` `Quotient.group` `instTopologicalSpace` `instIsTopologicalGroup`	—	`instIsTopologicalGroup` `IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace` `completeSpace_right'`
`completeSpace_right` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `IsTopologicalGroup.rightUniformSpace` `Quotient.group` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `instIsTopologicalGroup` `IsRightUniformGroup.toIsTopologicalGroup`	—	`IsRightUniformGroup.toIsTopologicalGroup` `UniformSpace.ext` `IsRightUniformGroup.uniformity_eq` `instIsTopologicalGroup` `completeSpace_right'`
`completeSpace_right'` 📖	mathematical	—	`CompleteSpace` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `IsTopologicalGroup.rightUniformSpace` `Quotient.group` `instTopologicalSpace` `instIsTopologicalGroup`	—	`instIsTopologicalGroup` `IsTopologicalGroup.exists_antitone_basis_nhds_one` `Filter.HasAntitoneBasis.map` `UniformSpace.complete_of_cauchySeq_tendsto` `Filter.comap.isCountablyGenerated` `FirstCountableTopology.nhds_generated_countable` `instFirstCountableTopology` `IsTopologicalGroup.toContinuousMul` `div_eq_mul_inv` `Filter.HasBasis.comap` `mk_one` `nhds_eq` `Filter.HasBasis.cauchySeq_iff` `LE.le.trans_lt` `le_max_left` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `LE.le.trans` `le_max_right` `LT.lt.le` `mul_inv_rev` `inv_inv` `mul_inv_cancel_left` `mk_mul` `mk_inv` `inv_div` `div_mul_cancel` `mk_surjective` `le_rfl` `Filter.HasAntitoneBasis.toHasBasis` `Filter.HasBasis.cauchySeq_iff'` `div_mul_div_cancel` `div_self'` `mem_of_mem_nhds` `Filter.HasAntitoneBasis.mem` `cauchySeq_tendsto_of_complete` `tendsto_nhds_of_cauchySeq_of_subseq` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `StrictMono.tendsto_atTop` `strictMono_nat_of_lt_succ` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_coinduced_rng`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_of_discrete` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Subgroup` `instSetLike`	—	`isDiscrete_iff_discreteTopology` `nhds_inter_eq_singleton_of_mem_discrete` `one_mem` `Filter.preimage_mem_comap` `isClosed_of_spaced_out` `T1Space.t0Space` `T2Space.t1Space` `Mathlib.Tactic.Contrapose.contrapose₄` `Set.mem_inter` `div_mem` `eq_of_div_eq_one`
`isUniformGroup` 📖	mathematical	—	`IsUniformGroup` `Subgroup` `SetLike.instMembership` `instSetLike` `instUniformSpaceSubtype` `toGroup`	—	`IsUniformGroup.comap` `MonoidHom.instMonoidHomClass`
`tendsto_coe_cofinite_of_discrete` 📖	mathematical	`IsDiscrete` `SetLike.coe` `Subgroup` `instSetLike`	`Filter.Tendsto` `SetLike.instMembership` `Filter.cofinite` `Filter.cocompact`	—	`IsClosed.tendsto_coe_cofinite_of_isDiscrete` `isClosed_of_discrete` `isDiscrete_iff_discreteTopology`

TendstoLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`TendstoLocallyUniformly`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformly` `uniformContinuous_add` `prodMk`
`div` 📖	mathematical	`TendstoLocallyUniformly`	`Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformly` `uniformContinuous_div` `prodMk`
`fun_add` 📖	mathematical	`TendstoLocallyUniformly`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add`
`fun_div` 📖	mathematical	`TendstoLocallyUniformly`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div`
`fun_inv` 📖	mathematical	`TendstoLocallyUniformly`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv`
`fun_mul` 📖	mathematical	`TendstoLocallyUniformly`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul`
`fun_neg` 📖	mathematical	`TendstoLocallyUniformly`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg`
`fun_sub` 📖	mathematical	`TendstoLocallyUniformly`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub`
`inv` 📖	mathematical	`TendstoLocallyUniformly`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformly` `uniformContinuous_inv`
`mul` 📖	mathematical	`TendstoLocallyUniformly`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformly` `uniformContinuous_mul` `prodMk`
`neg` 📖	mathematical	`TendstoLocallyUniformly`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformly` `uniformContinuous_neg`
`sub` 📖	mathematical	`TendstoLocallyUniformly`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformly` `uniformContinuous_sub` `prodMk`

TendstoLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`TendstoLocallyUniformlyOn`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformlyOn` `uniformContinuous_add` `prodMk`
`div` 📖	mathematical	`TendstoLocallyUniformlyOn`	`Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformlyOn` `uniformContinuous_div` `prodMk`
`fun_add` 📖	mathematical	`TendstoLocallyUniformlyOn`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add`
`fun_div` 📖	mathematical	`TendstoLocallyUniformlyOn`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div`
`fun_inv` 📖	mathematical	`TendstoLocallyUniformlyOn`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv`
`fun_mul` 📖	mathematical	`TendstoLocallyUniformlyOn`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul`
`fun_neg` 📖	mathematical	`TendstoLocallyUniformlyOn`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg`
`fun_sub` 📖	mathematical	`TendstoLocallyUniformlyOn`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub`
`inv` 📖	mathematical	`TendstoLocallyUniformlyOn`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformlyOn` `uniformContinuous_inv`
`mul` 📖	mathematical	`TendstoLocallyUniformlyOn`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformlyOn` `uniformContinuous_mul` `prodMk`
`neg` 📖	mathematical	`TendstoLocallyUniformlyOn`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformlyOn` `uniformContinuous_neg`
`sub` 📖	mathematical	`TendstoLocallyUniformlyOn`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_tendstoLocallyUniformlyOn` `uniformContinuous_sub` `prodMk`

TendstoUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`TendstoUniformly`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Filter.Eventually.diag_of_prod` `UniformContinuous.comp_tendstoUniformly` `uniformContinuous_add` `prodMk`
`div` 📖	mathematical	`TendstoUniformly`	`Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`Filter.Eventually.diag_of_prod` `UniformContinuous.comp_tendstoUniformly` `uniformContinuous_div` `prodMk`
`fun_add` 📖	mathematical	`TendstoUniformly`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add`
`fun_div` 📖	mathematical	`TendstoUniformly`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div`
`fun_inv` 📖	mathematical	`TendstoUniformly`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv`
`fun_mul` 📖	mathematical	`TendstoUniformly`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul`
`fun_neg` 📖	mathematical	`TendstoUniformly`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg`
`fun_sub` 📖	mathematical	`TendstoUniformly`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub`
`inv` 📖	mathematical	`TendstoUniformly`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`UniformContinuous.comp_tendstoUniformly` `uniformContinuous_inv`
`mul` 📖	mathematical	`TendstoUniformly`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Filter.Eventually.diag_of_prod` `UniformContinuous.comp_tendstoUniformly` `uniformContinuous_mul` `prodMk`
`neg` 📖	mathematical	`TendstoUniformly`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`UniformContinuous.comp_tendstoUniformly` `uniformContinuous_neg`
`sub` 📖	mathematical	`TendstoUniformly`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Filter.Eventually.diag_of_prod` `UniformContinuous.comp_tendstoUniformly` `uniformContinuous_sub` `prodMk`

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`TendstoUniformlyOn`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Filter.Eventually.diag_of_prod` `UniformContinuous.comp_tendstoUniformlyOn` `uniformContinuous_add` `prodMk`
`div` 📖	mathematical	`TendstoUniformlyOn`	`Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`Filter.Eventually.diag_of_prod` `UniformContinuous.comp_tendstoUniformlyOn` `uniformContinuous_div` `prodMk`
`fun_add` 📖	mathematical	`TendstoUniformlyOn`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add`
`fun_div` 📖	mathematical	`TendstoUniformlyOn`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div`
`fun_inv` 📖	mathematical	`TendstoUniformlyOn`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv`
`fun_mul` 📖	mathematical	`TendstoUniformlyOn`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul`
`fun_neg` 📖	mathematical	`TendstoUniformlyOn`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg`
`fun_sub` 📖	mathematical	`TendstoUniformlyOn`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub`
`inv` 📖	mathematical	`TendstoUniformlyOn`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`UniformContinuous.comp_tendstoUniformlyOn` `uniformContinuous_inv`
`mul` 📖	mathematical	`TendstoUniformlyOn`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Filter.Eventually.diag_of_prod` `UniformContinuous.comp_tendstoUniformlyOn` `uniformContinuous_mul` `prodMk`
`neg` 📖	mathematical	`TendstoUniformlyOn`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`UniformContinuous.comp_tendstoUniformlyOn` `uniformContinuous_neg`
`sub` 📖	mathematical	`TendstoUniformlyOn`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Filter.Eventually.diag_of_prod` `UniformContinuous.comp_tendstoUniformlyOn` `uniformContinuous_sub` `prodMk`

TendstoUniformlyOnFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`TendstoUniformlyOnFilter`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Filter.Eventually.diag_of_prod_left` `UniformContinuous.comp_tendstoUniformlyOnFilter` `uniformContinuous_add` `prodMk`
`div` 📖	mathematical	`TendstoUniformlyOnFilter`	`Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`Filter.Eventually.diag_of_prod_left` `UniformContinuous.comp_tendstoUniformlyOnFilter` `uniformContinuous_div` `prodMk`
`fun_add` 📖	mathematical	`TendstoUniformlyOnFilter`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add`
`fun_div` 📖	mathematical	`TendstoUniformlyOnFilter`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div`
`fun_inv` 📖	mathematical	`TendstoUniformlyOnFilter`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv`
`fun_mul` 📖	mathematical	`TendstoUniformlyOnFilter`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul`
`fun_neg` 📖	mathematical	`TendstoUniformlyOnFilter`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg`
`fun_sub` 📖	mathematical	`TendstoUniformlyOnFilter`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub`
`inv` 📖	mathematical	`TendstoUniformlyOnFilter`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`UniformContinuous.comp_tendstoUniformlyOnFilter` `uniformContinuous_inv`
`mul` 📖	mathematical	`TendstoUniformlyOnFilter`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Filter.Eventually.diag_of_prod_left` `UniformContinuous.comp_tendstoUniformlyOnFilter` `uniformContinuous_mul` `prodMk`
`neg` 📖	mathematical	`TendstoUniformlyOnFilter`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`UniformContinuous.comp_tendstoUniformlyOnFilter` `uniformContinuous_neg`
`sub` 📖	mathematical	`TendstoUniformlyOnFilter`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Filter.Eventually.diag_of_prod_left` `UniformContinuous.comp_tendstoUniformlyOnFilter` `uniformContinuous_sub` `prodMk`

UniformCauchySeqOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`UniformCauchySeqOn`	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_uniformCauchySeqOn` `uniformContinuous_add` `prod'`
`div` 📖	mathematical	`UniformCauchySeqOn`	`Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_uniformCauchySeqOn` `uniformContinuous_div` `prod'`
`fun_add` 📖	mathematical	`UniformCauchySeqOn`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add`
`fun_div` 📖	mathematical	`UniformCauchySeqOn`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div`
`fun_inv` 📖	mathematical	`UniformCauchySeqOn`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv`
`fun_mul` 📖	mathematical	`UniformCauchySeqOn`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul`
`fun_neg` 📖	mathematical	`UniformCauchySeqOn`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg`
`fun_sub` 📖	mathematical	`UniformCauchySeqOn`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub`
`inv` 📖	mathematical	`UniformCauchySeqOn`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`UniformContinuous.comp_uniformCauchySeqOn` `uniformContinuous_inv`
`mul` 📖	mathematical	`UniformCauchySeqOn`	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`UniformContinuous.comp_uniformCauchySeqOn` `uniformContinuous_mul` `prod'`
`neg` 📖	mathematical	`UniformCauchySeqOn`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`UniformContinuous.comp_uniformCauchySeqOn` `uniformContinuous_neg`
`sub` 📖	mathematical	`UniformCauchySeqOn`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`UniformContinuous.comp_uniformCauchySeqOn` `uniformContinuous_sub` `prod'`

UniformEquiv

Definitions

Name	Category	Theorems
`inv` 📖	CompOp	—
`neg` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_inv_leftUniformSpace` 📖	mathematical	—	`UniformSpace.comap` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.inv` `DivisionMonoid.toInvolutiveInv` `Group.toDivisionMonoid` `IsTopologicalGroup.leftUniformSpace` `IsTopologicalGroup.rightUniformSpace`	—	`UniformSpace.ext` `IsTopologicalGroup.toContinuousInv` `Homeomorph.comap_nhds_eq` `inv_one` `Filter.comap_comap` `inv_inv` `mul_inv_rev` `div_eq_mul_inv`
`comap_neg_leftUniformSpace` 📖	mathematical	—	`UniformSpace.comap` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.neg` `SubtractionMonoid.toInvolutiveNeg` `AddGroup.toSubtractionMonoid` `IsTopologicalAddGroup.leftUniformSpace` `IsTopologicalAddGroup.rightUniformSpace`	—	`UniformSpace.ext` `IsTopologicalAddGroup.toContinuousNeg` `Homeomorph.comap_nhds_eq` `neg_zero` `Filter.comap_comap` `neg_neg` `neg_add_rev` `sub_eq_add_neg`
`isUniformEmbedding_translate_add` 📖	mathematical	—	`IsUniformEmbedding` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`uniformity_translate_add` `Filter.comap_map` `AddRightCancelSemigroup.toIsRightCancelAdd` `add_left_injective`
`isUniformEmbedding_translate_mul` 📖	mathematical	—	`IsUniformEmbedding` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`uniformity_translate_mul` `Filter.comap_map` `RightCancelSemigroup.toIsRightCancelMul` `mul_left_injective`
`tendsto_div_comap_self` 📖	mathematical	`IsDenseInducing` `DFunLike.coe`	`Filter.Tendsto` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `Filter.comap` `nhds` `instTopologicalSpaceProd` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`map_div` `map_one` `MonoidHomClass.toOneHomClass` `div_self'` `Continuous.tendsto` `Continuous.comp` `ContinuousDiv.continuous_div'` `IsTopologicalGroup.to_continuousDiv` `continuous_swap` `IsDenseInducing.tendsto_comap_nhds_nhds`
`tendsto_sub_comap_self` 📖	mathematical	`IsDenseInducing` `DFunLike.coe`	`Filter.Tendsto` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Filter.comap` `nhds` `instTopologicalSpaceProd` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`map_sub` `map_zero` `AddMonoidHomClass.toZeroHomClass` `sub_self` `Continuous.tendsto` `Continuous.comp` `ContinuousSub.continuous_sub` `IsTopologicalAddGroup.to_continuousSub` `continuous_swap` `IsDenseInducing.tendsto_comap_nhds_nhds`
`topologicalAddGroup_is_uniform_of_compactSpace` 📖	mathematical	—	`IsUniformAddGroup` `IsTopologicalAddGroup.rightUniformSpace`	—	`IsUniformAddGroup.of_compactSpace` `IsTopologicalAddGroup.to_continuousSub`
`topologicalGroup_is_uniform_of_compactSpace` 📖	mathematical	—	`IsUniformGroup` `IsTopologicalGroup.rightUniformSpace`	—	`IsUniformGroup.of_compactSpace` `IsTopologicalGroup.to_continuousDiv`
`totallyBounded_iff_subset_finite_iUnion_nhds_one` 📖	mathematical	—	`TotallyBounded` `Set.Finite` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`Filter.HasBasis.totallyBounded_iff` `Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped` `Filter.basis_sets` `Set.iUnion_congr_Prop`
`totallyBounded_iff_subset_finite_iUnion_nhds_zero` 📖	mathematical	—	`TotallyBounded` `Set.Finite` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`Filter.HasBasis.totallyBounded_iff` `Filter.HasBasis.uniformity_of_nhds_zero_neg_add_swapped` `Filter.basis_sets` `Set.iUnion_congr_Prop` `Set.preimage_vadd_neg`
`totallyBounded_inv` 📖	mathematical	`TotallyBounded`	`Set` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Set.ext` `Set.image_inv_eq_inv` `TotallyBounded.image` `uniformContinuous_inv`
`totallyBounded_neg` 📖	mathematical	`TotallyBounded`	`Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Set.ext` `Set.mem_neg` `Set.image_neg_eq_neg` `TotallyBounded.image` `uniformContinuous_neg`

---

← Back to Index