Defs

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

Statistics

Metric	Count
Definitions IsLeftUniformAddGroup, IsLeftUniformGroup, IsRightUniformAddGroup, IsRightUniformGroup, leftUniformSpace, rightUniformSpace, toUniformSpace, leftUniformSpace, rightUniformSpace, toUniformSpace, IsUniformAddGroup, IsUniformGroup	12
Theorems isUniformInducing_of_isInducing, uniformContinuous_of_continuousAt_zero, instIsUniformAddGroup, uniformity_of_nhds_one, uniformity_of_nhds_one_inv_mul, uniformity_of_nhds_one_inv_mul_swapped, uniformity_of_nhds_one_swapped, uniformity_of_nhds_zero, uniformity_of_nhds_zero_neg_add, uniformity_of_nhds_zero_neg_add_swapped, uniformity_of_nhds_zero_swapped, conj_nhds_one, conj_nhds_zero, uniformity_add, uniformity_add_iff_left, uniformity_add_iff_right, uniformity_div, uniformity_inv, uniformity_inv_iff, uniformity_mul, uniformity_mul_iff_left, uniformity_mul_iff_right, uniformity_neg, uniformity_neg_iff, uniformity_sub, uniformContinuous_prod, uniformContinuous_sum, toIsTopologicalAddGroup, uniformity_eq, toIsTopologicalGroup, uniformity_eq, toIsTopologicalAddGroup, uniformity_eq, toIsTopologicalGroup, uniformity_eq, ext, ext_iff, isLeftUniformAddGroup, isRightUniformAddGroup, mk', rightUniformSpace_eq, toUniformSpace_eq, to_topologicalAddGroup, uniformContinuous_iff_isOpen_ker, uniformContinuous_sub, uniformity_countably_generated, ext, ext_iff, isLeftUniformGroup, isRightUniformGroup, mk', of_left_right, rightUniformSpace_eq, toUniformSpace_eq, to_topologicalGroup, uniformContinuous_div, uniformContinuous_iff_isOpen_ker, uniformity_countably_generated, isUniformInducing_of_isInducing, uniformContinuous_of_continuousAt_one, instIsUniformGroup, add, add_const, const_add, const_mul, const_nsmul, const_zsmul, div, div_const, inv, mul, mul_const, neg, pow_const, sub, sub_const, zpow_const, comap_conj_nhds_one, comap_conj_nhds_zero, comm_topologicalGroup_is_uniform, eventually_forall_conj_nhds_one, isUniformAddGroup_of_addCommGroup, isUniformGroup_iff_left_right, isUniformGroup_of_commGroup, tendsto_conj_nhds_one, tendsto_conj_nhds_zero, uniformContinuous_add, uniformContinuous_addMonoidHom_of_continuous, uniformContinuous_add_left, uniformContinuous_add_right, uniformContinuous_const_nsmul, uniformContinuous_const_zsmul, uniformContinuous_div, uniformContinuous_div_const, uniformContinuous_inv, uniformContinuous_monoidHom_of_continuous, uniformContinuous_mul, uniformContinuous_mul_left, uniformContinuous_mul_right, uniformContinuous_neg, uniformContinuous_of_continuousAt_one, uniformContinuous_of_continuousAt_zero, uniformContinuous_of_tendsto_one, uniformContinuous_of_tendsto_zero, uniformContinuous_pow_const, uniformContinuous_sub, uniformContinuous_sub_const, uniformContinuous_zpow_const, uniformity_eq_comap_add_neg_nhds_zero, uniformity_eq_comap_add_neg_nhds_zero_swapped, uniformity_eq_comap_inv_mul_nhds_one, uniformity_eq_comap_inv_mul_nhds_one_swapped, uniformity_eq_comap_mul_inv_nhds_one, uniformity_eq_comap_mul_inv_nhds_one_swapped, uniformity_eq_comap_neg_add_nhds_zero, uniformity_eq_comap_neg_add_nhds_zero_swapped, uniformity_eq_comap_nhds_one, uniformity_eq_comap_nhds_one', uniformity_eq_comap_nhds_one_left, uniformity_eq_comap_nhds_one_swapped, uniformity_eq_comap_nhds_zero, uniformity_eq_comap_nhds_zero', uniformity_eq_comap_nhds_zero_left, uniformity_eq_comap_nhds_zero_swapped, uniformity_translate_add, uniformity_translate_mul	126
Total	138

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUniformInducing_of_isInducing 📖	mathematical	Topology.IsInducing UniformSpace.toTopologicalSpace DFunLike.coe	IsUniformInducing	—	uniformity_eq_comap_nhds_zero IsUniformAddGroup.isRightUniformAddGroup Filter.comap_comap Topology.IsInducing.nhds_eq_comap map_zero AddMonoidHomClass.toZeroHomClass map_sub
uniformContinuous_of_continuousAt_zero 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	UniformContinuous	—	uniformContinuous_of_continuousAt_zero instAddMonoidHomClass

AddOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup AddOpposite instUniformSpaceAddOpposite instAddGroup	—	UniformContinuous.comp uniformContinuous_op UniformContinuous.add UniformContinuous.neg uniformContinuous_unop uniformContinuous_snd uniformContinuous_fst

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformity_of_nhds_one 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	uniformity setOf Set Set.instMembership DivInvMonoid.toDiv Group.toDivInvMonoid	—	uniformity_eq_comap_nhds_one IsUniformGroup.isRightUniformGroup comap
uniformity_of_nhds_one_inv_mul 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	uniformity setOf Set Set.instMembership MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv	—	uniformity_eq_comap_inv_mul_nhds_one IsUniformGroup.isLeftUniformGroup comap
uniformity_of_nhds_one_inv_mul_swapped 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	uniformity setOf Set Set.instMembership MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv	—	uniformity_eq_comap_inv_mul_nhds_one_swapped IsUniformGroup.isLeftUniformGroup comap
uniformity_of_nhds_one_swapped 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	uniformity setOf Set Set.instMembership DivInvMonoid.toDiv Group.toDivInvMonoid	—	uniformity_eq_comap_nhds_one_swapped IsUniformGroup.isRightUniformGroup comap
uniformity_of_nhds_zero 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	uniformity setOf Set Set.instMembership SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	uniformity_eq_comap_nhds_zero IsUniformAddGroup.isRightUniformAddGroup comap
uniformity_of_nhds_zero_neg_add 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	uniformity setOf Set Set.instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg	—	uniformity_eq_comap_neg_add_nhds_zero IsUniformAddGroup.isLeftUniformAddGroup comap
uniformity_of_nhds_zero_neg_add_swapped 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	uniformity setOf Set Set.instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg	—	uniformity_eq_comap_neg_add_nhds_zero_swapped IsUniformAddGroup.isLeftUniformAddGroup comap
uniformity_of_nhds_zero_swapped 📖	mathematical	Filter.HasBasis nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	uniformity setOf Set Set.instMembership SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	uniformity_eq_comap_nhds_zero_swapped IsUniformAddGroup.isRightUniformAddGroup comap

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_nhds_one 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Pi.instInv InvOneClass.toInv	—	Filter.tendsto_comap_iff comp tendsto_conj_nhds_one
conj_nhds_zero 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Pi.instNeg NegZeroClass.toNeg	—	Filter.tendsto_comap_iff comp tendsto_conj_nhds_zero
uniformity_add 📖	mathematical	Filter.Tendsto uniformity	Pi.instAdd Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	uniformity_prod_eq_prod Filter.tendsto_map'_iff uniformContinuous_add comp prodMk
uniformity_add_iff_left 📖	mathematical	Filter.Tendsto uniformity	Pi.instAdd Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	add_neg_cancel_right uniformity_add uniformity_neg
uniformity_add_iff_right 📖	mathematical	Filter.Tendsto uniformity	Pi.instAdd Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	neg_add_cancel_left uniformity_add uniformity_neg
uniformity_div 📖	mathematical	Filter.Tendsto uniformity	Pi.instDiv Prod.instDiv DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv uniformity_mul uniformity_inv
uniformity_inv 📖	mathematical	Filter.Tendsto uniformity	Pi.instInv Prod.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	uniformContinuous_inv comp
uniformity_inv_iff 📖	mathematical	—	Filter.Tendsto Pi.instInv Prod.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid uniformity	—	uniformity_inv inv_inv
uniformity_mul 📖	mathematical	Filter.Tendsto uniformity	Pi.instMul Prod.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	uniformity_prod_eq_prod uniformContinuous_mul comp prodMk
uniformity_mul_iff_left 📖	mathematical	Filter.Tendsto uniformity	Pi.instMul Prod.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	mul_inv_cancel_right uniformity_mul uniformity_inv
uniformity_mul_iff_right 📖	mathematical	Filter.Tendsto uniformity	Pi.instMul Prod.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	inv_mul_cancel_left uniformity_mul uniformity_inv
uniformity_neg 📖	mathematical	Filter.Tendsto uniformity	Pi.instNeg Prod.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	uniformContinuous_neg comp
uniformity_neg_iff 📖	mathematical	—	Filter.Tendsto Pi.instNeg Prod.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid uniformity	—	uniformity_neg neg_neg
uniformity_sub 📖	mathematical	Filter.Tendsto uniformity	Pi.instSub Prod.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg uniformity_add uniformity_neg

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformContinuous_prod 📖	mathematical	UniformContinuous	prod CommGroup.toCommMonoid	—	cons_induction uniformContinuous_const prod_cons UniformContinuous.mul
uniformContinuous_sum 📖	mathematical	UniformContinuous	sum AddCommGroup.toAddCommMonoid	—	cons_induction uniformContinuous_const sum_cons UniformContinuous.add mem_cons

IsLeftUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup UniformSpace.toTopologicalSpace	—	—
uniformity_eq 📖	mathematical	—	uniformity Filter.comap AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero	—	—

IsLeftUniformGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsTopologicalGroup 📖	mathematical	—	IsTopologicalGroup UniformSpace.toTopologicalSpace	—	—
uniformity_eq 📖	mathematical	—	uniformity Filter.comap MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne	—	—

IsRightUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup UniformSpace.toTopologicalSpace	—	—
uniformity_eq 📖	mathematical	—	uniformity Filter.comap AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero	—	—

IsRightUniformGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsTopologicalGroup 📖	mathematical	—	IsTopologicalGroup UniformSpace.toTopologicalSpace	—	—
uniformity_eq 📖	mathematical	—	uniformity Filter.comap MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne	—	—

IsTopologicalAddGroup

Definitions

Name	Category	Theorems
leftUniformSpace 📖	CompOp	7 math math: AddOpposite.comap_op_leftUniformSpace, QuotientAddGroup.completeSpace_left, comap_neg_leftUniformSpace, uniformity_eq_comap_nhds_zero_left, completeSpace_rightUniformSpace_iff_leftUniformSpace, AddOpposite.comap_op_rightUniformSpace, QuotientAddGroup.completeSpace_left'
rightUniformSpace 📖	CompOp	12 math math: AddOpposite.comap_op_leftUniformSpace, IsUniformAddGroup.toUniformSpace_eq, QuotientAddGroup.completeSpace_right', Valued.toUniformSpace_eq, IsUniformAddGroup.rightUniformSpace_eq, QuotientAddGroup.completeSpace_right, comap_neg_leftUniformSpace, isUniformAddGroup_of_addCommGroup, topologicalAddGroup_is_uniform_of_compactSpace, completeSpace_rightUniformSpace_iff_leftUniformSpace, uniformity_eq_comap_nhds_zero', AddOpposite.comap_op_rightUniformSpace
toUniformSpace 📖	CompOp	—

IsTopologicalGroup

Definitions

Name	Category	Theorems
leftUniformSpace 📖	CompOp	7 math math: QuotientGroup.completeSpace_left, comap_inv_leftUniformSpace, completeSpace_rightUniformSpace_iff_leftUniformSpace, QuotientGroup.completeSpace_left', MulOpposite.comap_op_leftUniformSpace, MulOpposite.comap_op_rightUniformSpace, uniformity_eq_comap_nhds_one_left
rightUniformSpace 📖	CompOp	12 math math: comap_inv_leftUniformSpace, IsUniformGroup.toUniformSpace_eq, QuotientGroup.completeSpace_right, QuotientGroup.completeSpace_right', completeSpace_rightUniformSpace_iff_leftUniformSpace, comm_topologicalGroup_is_uniform, IsUniformGroup.rightUniformSpace_eq, MulOpposite.comap_op_leftUniformSpace, isUniformGroup_of_commGroup, MulOpposite.comap_op_rightUniformSpace, topologicalGroup_is_uniform_of_compactSpace, uniformity_eq_comap_nhds_one'
toUniformSpace 📖	CompOp	—

IsUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—	UniformSpace.ext uniformity_eq_comap_nhds_zero isRightUniformAddGroup
ext_iff 📖	mathematical	—	nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	ext
isLeftUniformAddGroup 📖	mathematical	—	IsLeftUniformAddGroup	—	to_topologicalAddGroup eq_of_forall_le_iff nhds_eq_comap_uniformity Filter.comap_comap Filter.tendsto_iff_comap Filter.Tendsto.uniformity_add_iff_right tendsto_diag_uniformity Filter.tendsto_id' add_zero add_neg_cancel_left
isRightUniformAddGroup 📖	mathematical	—	IsRightUniformAddGroup	—	to_topologicalAddGroup eq_of_forall_le_iff nhds_eq_comap_uniformity Filter.comap_comap Filter.tendsto_iff_comap Filter.Tendsto.uniformity_add_iff_left tendsto_diag_uniformity Filter.tendsto_id' zero_add neg_add_cancel_right
mk' 📖	mathematical	UniformContinuous instUniformSpaceProd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	IsUniformAddGroup	—	sub_eq_add_neg UniformContinuous.comp UniformContinuous.prodMk uniformContinuous_fst uniformContinuous_snd
rightUniformSpace_eq 📖	mathematical	—	IsTopologicalAddGroup.rightUniformSpace UniformSpace.toTopologicalSpace to_topologicalAddGroup	—	UniformSpace.ext to_topologicalAddGroup uniformity_eq_comap_nhds_zero' uniformity_eq_comap_nhds_zero isRightUniformAddGroup
toUniformSpace_eq 📖	mathematical	—	IsTopologicalAddGroup.rightUniformSpace UniformSpace.toTopologicalSpace to_topologicalAddGroup	—	rightUniformSpace_eq
to_topologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup UniformSpace.toTopologicalSpace	—	UniformContinuous.continuous uniformContinuous_add uniformContinuous_neg
uniformContinuous_iff_isOpen_ker 📖	mathematical	—	UniformContinuous DFunLike.coe IsOpen UniformSpace.toTopologicalSpace SetLike.coe AddSubgroup AddSubgroup.instSetLike AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHomClass.toAddMonoidHom AddZeroClass.toAddZero	—	IsOpen.preimage UniformContinuous.continuous isOpen_discrete uniformContinuous_of_continuousAt_zero ContinuousAt.eq_1 nhds_discrete map_zero AddMonoidHomClass.toZeroHomClass Filter.tendsto_pure IsOpen.mem_nhds
uniformContinuous_sub 📖	mathematical	—	UniformContinuous instUniformSpaceProd SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—
uniformity_countably_generated 📖	mathematical	—	Filter.IsCountablyGenerated uniformity	—	uniformity_eq_comap_nhds_zero isRightUniformAddGroup Filter.comap.isCountablyGenerated

IsUniformGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—	UniformSpace.ext uniformity_eq_comap_nhds_one isRightUniformGroup
ext_iff 📖	mathematical	—	nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	ext
isLeftUniformGroup 📖	mathematical	—	IsLeftUniformGroup	—	to_topologicalGroup eq_of_forall_le_iff nhds_eq_comap_uniformity Filter.comap_comap Filter.tendsto_iff_comap Filter.Tendsto.uniformity_mul_iff_right tendsto_diag_uniformity Filter.tendsto_id' mul_one mul_inv_cancel_left
isRightUniformGroup 📖	mathematical	—	IsRightUniformGroup	—	to_topologicalGroup eq_of_forall_le_iff nhds_eq_comap_uniformity Filter.comap_comap Filter.tendsto_iff_comap Filter.Tendsto.uniformity_mul_iff_left tendsto_diag_uniformity Filter.tendsto_id' one_mul inv_mul_cancel_right
mk' 📖	mathematical	UniformContinuous instUniformSpaceProd MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	IsUniformGroup	—	div_eq_mul_inv UniformContinuous.comp UniformContinuous.prodMk uniformContinuous_fst uniformContinuous_snd
of_left_right 📖	mathematical	—	IsUniformGroup	—	mul_assoc mul_inv_cancel_left one_mul Filter.Tendsto.mul IsTopologicalGroup.toContinuousMul IsLeftUniformGroup.toIsTopologicalGroup uniformity_eq_comap_inv_mul_nhds_one Filter.Tendsto.comp Filter.tendsto_comap Filter.tendsto_fst uniformity_eq_comap_inv_mul_nhds_one_swapped Filter.tendsto_snd Filter.Tendsto.conj_nhds_one UniformContinuous.eq_1 uniformity_eq_comap_mul_inv_nhds_one Filter.tendsto_comap_iff uniformity_prod_eq_prod Filter.tendsto_map'_iff div_eq_mul_inv mul_inv_rev inv_inv
rightUniformSpace_eq 📖	mathematical	—	IsTopologicalGroup.rightUniformSpace UniformSpace.toTopologicalSpace to_topologicalGroup	—	UniformSpace.ext to_topologicalGroup uniformity_eq_comap_nhds_one' uniformity_eq_comap_nhds_one isRightUniformGroup
toUniformSpace_eq 📖	mathematical	—	IsTopologicalGroup.rightUniformSpace UniformSpace.toTopologicalSpace to_topologicalGroup	—	rightUniformSpace_eq
to_topologicalGroup 📖	mathematical	—	IsTopologicalGroup UniformSpace.toTopologicalSpace	—	UniformContinuous.continuous uniformContinuous_mul uniformContinuous_inv
uniformContinuous_div 📖	mathematical	—	UniformContinuous instUniformSpaceProd DivInvMonoid.toDiv Group.toDivInvMonoid	—	—
uniformContinuous_iff_isOpen_ker 📖	mathematical	—	UniformContinuous DFunLike.coe IsOpen UniformSpace.toTopologicalSpace SetLike.coe Subgroup Subgroup.instSetLike MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHomClass.toMonoidHom MulOneClass.toMulOne	—	IsOpen.preimage UniformContinuous.continuous isOpen_discrete uniformContinuous_of_continuousAt_one ContinuousAt.eq_1 nhds_discrete map_one MonoidHomClass.toOneHomClass Filter.tendsto_pure IsOpen.mem_nhds
uniformity_countably_generated 📖	mathematical	—	Filter.IsCountablyGenerated uniformity	—	uniformity_eq_comap_nhds_one isRightUniformGroup Filter.comap.isCountablyGenerated

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUniformInducing_of_isInducing 📖	mathematical	Topology.IsInducing UniformSpace.toTopologicalSpace DFunLike.coe	IsUniformInducing	—	uniformity_eq_comap_nhds_one IsUniformGroup.isRightUniformGroup Filter.comap_comap Topology.IsInducing.nhds_eq_comap map_one MonoidHomClass.toOneHomClass map_div
uniformContinuous_of_continuousAt_one 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	UniformContinuous	—	uniformContinuous_of_continuousAt_one instMonoidHomClass

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsUniformGroup 📖	mathematical	—	IsUniformGroup MulOpposite instUniformSpaceMulOpposite instGroup	—	UniformContinuous.comp uniformContinuous_op UniformContinuous.mul UniformContinuous.inv uniformContinuous_unop uniformContinuous_snd uniformContinuous_fst

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	UniformContinuous	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	sub neg sub_neg_eq_add
add_const 📖	mathematical	UniformContinuous	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	add uniformContinuous_const
const_add 📖	mathematical	UniformContinuous	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	add uniformContinuous_const
const_mul 📖	mathematical	UniformContinuous	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	mul uniformContinuous_const
const_nsmul 📖	mathematical	UniformContinuous	AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	zero_nsmul uniformContinuous_const succ_nsmul' add
const_zsmul 📖	mathematical	UniformContinuous	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	natCast_zsmul const_nsmul negSucc_zsmul neg
div 📖	mathematical	UniformContinuous	DivInvMonoid.toDiv Group.toDivInvMonoid	—	comp uniformContinuous_div prodMk
div_const 📖	mathematical	UniformContinuous	DivInvMonoid.toDiv Group.toDivInvMonoid	—	div uniformContinuous_const
inv 📖	mathematical	UniformContinuous	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	div uniformContinuous_const one_div
mul 📖	mathematical	UniformContinuous	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	div inv div_inv_eq_mul
mul_const 📖	mathematical	UniformContinuous	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	mul uniformContinuous_const
neg 📖	mathematical	UniformContinuous	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	sub uniformContinuous_const zero_sub
pow_const 📖	mathematical	UniformContinuous	Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	pow_zero uniformContinuous_const pow_succ' mul
sub 📖	mathematical	UniformContinuous	SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	comp uniformContinuous_sub prodMk
sub_const 📖	mathematical	UniformContinuous	SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub uniformContinuous_const
zpow_const 📖	mathematical	UniformContinuous	DivInvMonoid.toZPow Group.toDivInvMonoid	—	zpow_natCast pow_const zpow_negSucc inv

(root)

Definitions

Name	Category	Theorems
IsLeftUniformAddGroup 📖	CompData	1 math math: IsUniformAddGroup.isLeftUniformAddGroup
IsLeftUniformGroup 📖	CompData	2 math math: isUniformGroup_iff_left_right, IsUniformGroup.isLeftUniformGroup
IsRightUniformAddGroup 📖	CompData	1 math math: IsUniformAddGroup.isRightUniformAddGroup
IsRightUniformGroup 📖	CompData	2 math math: isUniformGroup_iff_left_right, IsUniformGroup.isRightUniformGroup
IsUniformAddGroup 📖	CompData	35 math math: ContinuousAlternatingMap.instIsUniformAddGroup, ContinuousLinearMapWOT.instIsUniformAddGroup, Prod.instIsUniformAddGroup, WithCStarModule.instIsUniformAddGroup, CStarMatrix.instIsUniformAddGroup, TestFunction.instIsUniformAddGroup, isUniformAddGroup_inf, instIsUniformAddGroupUniformFun, AddSubgroup.isUniformAddGroup, IsUniformInducing.isUniformAddGroup, IsUniformAddGroup.of_compactSpace, ContDiffMapSupportedIn.isUniformAddGroup, ContinuousLinearMap.isUniformAddGroup, Valued.toIsUniformAddGroup, ContinuousMultilinearMap.instIsUniformAddGroup, UniformConvergenceCLM.instIsUniformAddGroup, IsUniformAddGroup.mk', MvPowerSeries.WithPiTopology.instIsUniformAddGroup, TrivSqZeroExt.instIsUniformAddGroup, SeparationQuotient.instIsUniformAddGroup, isUniformAddGroup_of_addCommGroup, IsUniformAddGroup.comap, instIsUniformAddGroupReal, instIsUniformAddGroupUniformOnFun, UniformSpace.Completion.isUniformAddGroup, topologicalAddGroup_is_uniform_of_compactSpace, AddOpposite.instIsUniformAddGroup, PowerSeries.WithPiTopology.instIsUniformAddGroup, Matrix.instIsUniformAddGroup, instIsUniformAddGroupOfDiscreteUniformity, Rat.instIsUniformAddGroup, AddGroupFilterBasis.isUniformAddGroup, WithIdeal.instIsUniformAddGroup, SeminormedAddCommGroup.to_isUniformAddGroup, SchwartzMap.instIsUniformAddGroup
IsUniformGroup 📖	CompData	19 math math: IsUniformGroup.mk', isUniformGroup_iff_left_right, isUniformGroup_inf, SeparationQuotient.instIsUniformGroup, Prod.instIsUniformGroup, Subgroup.isUniformGroup, instIsUniformGroupUniformOnFun, MulOpposite.instIsUniformGroup, comm_topologicalGroup_is_uniform, IsUniformGroup.comap, Circle.instIsUniformGroup, IsUniformInducing.isUniformGroup, IsUniformGroup.of_compactSpace, instIsUniformGroupOfDiscreteUniformity, instIsUniformGroupUniformFun, isUniformGroup_of_commGroup, IsUniformGroup.of_left_right, SeminormedCommGroup.to_isUniformGroup, topologicalGroup_is_uniform_of_compactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_conj_nhds_one 📖	mathematical	—	Filter.comap MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne	—	Equiv.mulLeft_symm mul_inv_cancel_left Filter.comap_injective Equiv.surjective Filter.comap_comap uniformity_eq_comap_inv_mul_nhds_one uniformity_eq_comap_mul_inv_nhds_one
comap_conj_nhds_zero 📖	mathematical	—	Filter.comap AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero	—	Equiv.addLeft_symm add_neg_cancel_left Filter.comap_injective Equiv.surjective Filter.comap_comap uniformity_eq_comap_neg_add_nhds_zero uniformity_eq_comap_add_neg_nhds_zero
comm_topologicalGroup_is_uniform 📖	mathematical	—	IsUniformGroup IsTopologicalGroup.rightUniformSpace CommGroup.toGroup	—	isUniformGroup_of_commGroup
eventually_forall_conj_nhds_one 📖	—	Filter.Eventually nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—	Filter.Tendsto.eventually tendsto_conj_nhds_one IsUniformGroup.isLeftUniformGroup IsUniformGroup.isRightUniformGroup
isUniformAddGroup_of_addCommGroup 📖	mathematical	—	IsUniformAddGroup IsTopologicalAddGroup.rightUniformSpace AddCommGroup.toAddGroup	—	uniformity_prod_eq_prod Filter.prod_comap_comap_eq nhds_prod_eq Filter.tendsto_comap_iff sub_sub_sub_comm Filter.tendsto_map'_iff Filter.Tendsto.comp Continuous.tendsto' ContinuousSub.continuous_sub IsTopologicalAddGroup.to_continuousSub sub_zero Filter.tendsto_comap
isUniformGroup_iff_left_right 📖	mathematical	—	IsUniformGroup IsLeftUniformGroup IsRightUniformGroup	—	IsUniformGroup.isLeftUniformGroup IsUniformGroup.isRightUniformGroup IsUniformGroup.of_left_right
isUniformGroup_of_commGroup 📖	mathematical	—	IsUniformGroup IsTopologicalGroup.rightUniformSpace CommGroup.toGroup	—	uniformity_prod_eq_prod Filter.prod_comap_comap_eq div_div_div_comm Filter.Tendsto.comp Continuous.tendsto' ContinuousDiv.continuous_div' IsTopologicalGroup.to_continuousDiv div_one Filter.tendsto_comap
tendsto_conj_nhds_one 📖	mathematical	—	Filter.Tendsto MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Filter.comap nhds UniformSpace.toTopologicalSpace InvOneClass.toOne	—	Filter.tendsto_iff_comap comap_conj_nhds_one le_refl
tendsto_conj_nhds_zero 📖	mathematical	—	Filter.Tendsto AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Filter.comap nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero	—	Filter.tendsto_iff_comap comap_conj_nhds_zero le_refl
uniformContinuous_add 📖	mathematical	—	UniformContinuous instUniformSpaceProd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	UniformContinuous.add uniformContinuous_fst uniformContinuous_snd
uniformContinuous_addMonoidHom_of_continuous 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe	UniformContinuous	—	uniformContinuous_of_tendsto_zero Continuous.tendsto map_zero AddMonoidHomClass.toZeroHomClass
uniformContinuous_add_left 📖	mathematical	—	UniformContinuous AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	UniformContinuous.const_add uniformContinuous_id
uniformContinuous_add_right 📖	mathematical	—	UniformContinuous AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	UniformContinuous.add_const uniformContinuous_id
uniformContinuous_const_nsmul 📖	mathematical	—	UniformContinuous AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	UniformContinuous.const_nsmul uniformContinuous_id
uniformContinuous_const_zsmul 📖	mathematical	—	UniformContinuous SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	UniformContinuous.const_zsmul uniformContinuous_id
uniformContinuous_div 📖	mathematical	—	UniformContinuous instUniformSpaceProd DivInvMonoid.toDiv Group.toDivInvMonoid	—	IsUniformGroup.uniformContinuous_div
uniformContinuous_div_const 📖	mathematical	—	UniformContinuous DivInvMonoid.toDiv Group.toDivInvMonoid	—	UniformContinuous.div_const uniformContinuous_id
uniformContinuous_inv 📖	mathematical	—	UniformContinuous InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	UniformContinuous.inv uniformContinuous_id
uniformContinuous_monoidHom_of_continuous 📖	mathematical	Continuous UniformSpace.toTopologicalSpace DFunLike.coe	UniformContinuous	—	uniformContinuous_of_tendsto_one Continuous.tendsto map_one MonoidHomClass.toOneHomClass
uniformContinuous_mul 📖	mathematical	—	UniformContinuous instUniformSpaceProd MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	UniformContinuous.mul uniformContinuous_fst uniformContinuous_snd
uniformContinuous_mul_left 📖	mathematical	—	UniformContinuous MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	UniformContinuous.const_mul uniformContinuous_id
uniformContinuous_mul_right 📖	mathematical	—	UniformContinuous MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	UniformContinuous.mul_const uniformContinuous_id
uniformContinuous_neg 📖	mathematical	—	UniformContinuous NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	UniformContinuous.neg uniformContinuous_id
uniformContinuous_of_continuousAt_one 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace DFunLike.coe InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	UniformContinuous	—	uniformContinuous_of_tendsto_one map_one MonoidHomClass.toOneHomClass ContinuousAt.tendsto
uniformContinuous_of_continuousAt_zero 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace DFunLike.coe NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	UniformContinuous	—	uniformContinuous_of_tendsto_zero map_zero AddMonoidHomClass.toZeroHomClass ContinuousAt.tendsto
uniformContinuous_of_tendsto_one 📖	mathematical	Filter.Tendsto DFunLike.coe nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	UniformContinuous	—	map_div UniformContinuous.eq_1 uniformity_eq_comap_nhds_one IsUniformGroup.isRightUniformGroup Filter.tendsto_comap_iff Filter.Tendsto.comp Filter.tendsto_comap
uniformContinuous_of_tendsto_zero 📖	mathematical	Filter.Tendsto DFunLike.coe nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	UniformContinuous	—	map_sub UniformContinuous.eq_1 uniformity_eq_comap_nhds_zero IsUniformAddGroup.isRightUniformAddGroup Filter.tendsto_comap_iff Filter.Tendsto.comp Filter.tendsto_comap
uniformContinuous_pow_const 📖	mathematical	—	UniformContinuous Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	UniformContinuous.pow_const uniformContinuous_id
uniformContinuous_sub 📖	mathematical	—	UniformContinuous instUniformSpaceProd SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	IsUniformAddGroup.uniformContinuous_sub
uniformContinuous_sub_const 📖	mathematical	—	UniformContinuous SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	UniformContinuous.sub_const uniformContinuous_id
uniformContinuous_zpow_const 📖	mathematical	—	UniformContinuous DivInvMonoid.toZPow Group.toDivInvMonoid	—	UniformContinuous.zpow_const uniformContinuous_id
uniformity_eq_comap_add_neg_nhds_zero 📖	mathematical	—	uniformity Filter.comap AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero	—	IsRightUniformAddGroup.uniformity_eq
uniformity_eq_comap_add_neg_nhds_zero_swapped 📖	mathematical	—	uniformity Filter.comap AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero	—	comap_swap_uniformity uniformity_eq_comap_add_neg_nhds_zero Filter.comap_comap
uniformity_eq_comap_inv_mul_nhds_one 📖	mathematical	—	uniformity Filter.comap MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne	—	IsLeftUniformGroup.uniformity_eq
uniformity_eq_comap_inv_mul_nhds_one_swapped 📖	mathematical	—	uniformity Filter.comap MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne	—	comap_swap_uniformity uniformity_eq_comap_inv_mul_nhds_one Filter.comap_comap
uniformity_eq_comap_mul_inv_nhds_one 📖	mathematical	—	uniformity Filter.comap MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne	—	IsRightUniformGroup.uniformity_eq
uniformity_eq_comap_mul_inv_nhds_one_swapped 📖	mathematical	—	uniformity Filter.comap MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne	—	comap_swap_uniformity uniformity_eq_comap_mul_inv_nhds_one Filter.comap_comap
uniformity_eq_comap_neg_add_nhds_zero 📖	mathematical	—	uniformity Filter.comap AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero	—	IsLeftUniformAddGroup.uniformity_eq
uniformity_eq_comap_neg_add_nhds_zero_swapped 📖	mathematical	—	uniformity Filter.comap AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero	—	comap_swap_uniformity uniformity_eq_comap_neg_add_nhds_zero Filter.comap_comap
uniformity_eq_comap_nhds_one 📖	mathematical	—	uniformity Filter.comap DivInvMonoid.toDiv Group.toDivInvMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	div_eq_mul_inv uniformity_eq_comap_mul_inv_nhds_one
uniformity_eq_comap_nhds_one' 📖	mathematical	—	uniformity IsTopologicalGroup.rightUniformSpace Filter.comap DivInvMonoid.toDiv Group.toDivInvMonoid nhds InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
uniformity_eq_comap_nhds_one_left 📖	mathematical	—	uniformity IsTopologicalGroup.leftUniformSpace Filter.comap MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid nhds InvOneClass.toOne	—	—
uniformity_eq_comap_nhds_one_swapped 📖	mathematical	—	uniformity Filter.comap DivInvMonoid.toDiv Group.toDivInvMonoid nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	comap_swap_uniformity uniformity_eq_comap_nhds_one Filter.comap_comap
uniformity_eq_comap_nhds_zero 📖	mathematical	—	uniformity Filter.comap SubNegMonoid.toSub AddGroup.toSubNegMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	sub_eq_add_neg uniformity_eq_comap_add_neg_nhds_zero
uniformity_eq_comap_nhds_zero' 📖	mathematical	—	uniformity IsTopologicalAddGroup.rightUniformSpace Filter.comap SubNegMonoid.toSub AddGroup.toSubNegMonoid nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
uniformity_eq_comap_nhds_zero_left 📖	mathematical	—	uniformity IsTopologicalAddGroup.leftUniformSpace Filter.comap AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid nhds NegZeroClass.toZero	—	—
uniformity_eq_comap_nhds_zero_swapped 📖	mathematical	—	uniformity Filter.comap SubNegMonoid.toSub AddGroup.toSubNegMonoid nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	comap_swap_uniformity uniformity_eq_comap_nhds_zero Filter.comap_comap
uniformity_translate_add 📖	mathematical	—	Filter.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid uniformity	—	le_antisymm UniformContinuous.add uniformContinuous_id uniformContinuous_const Filter.map_map neg_add_cancel_right Filter.map_id' Filter.map_mono
uniformity_translate_mul 📖	mathematical	—	Filter.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid uniformity	—	le_antisymm UniformContinuous.mul uniformContinuous_id uniformContinuous_const Filter.map_map inv_mul_cancel_right Filter.map_id' Filter.map_mono

---

← Back to Index