Defs

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

Statistics

Metric	Count
Definitions ContinuousDiv, ContinuousInv, ContinuousNeg, ContinuousSub, IsTopologicalAddGroup, IsTopologicalGroup	6
Theorems div', inv, neg, sub, div', inv, neg, sub, continuous_div', continuous_inv, continuous_neg, div', inv, neg, sub, continuous_sub, div', inv, neg, sub, div', inv, neg, sub, toContinuousAdd, toContinuousNeg, to_continuousSub, toContinuousInv, toContinuousMul, to_continuousDiv	30
Total	36

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div' 📖	—	Continuous	—	—	comp₂ ContinuousDiv.continuous_div'
inv 📖	—	Continuous	—	—	comp ContinuousInv.continuous_inv
neg 📖	—	Continuous	—	—	comp ContinuousNeg.continuous_neg
sub 📖	—	Continuous	—	—	comp₂ ContinuousSub.continuous_sub

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div' 📖	—	ContinuousAt	—	—	Filter.Tendsto.div'
inv 📖	—	ContinuousAt	—	—	Filter.Tendsto.inv
neg 📖	—	ContinuousAt	—	—	Filter.Tendsto.neg
sub 📖	—	ContinuousAt	—	—	Filter.Tendsto.sub

ContinuousDiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_div' 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	—

ContinuousInv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_inv 📖	mathematical	—	Continuous	—	—

ContinuousNeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_neg 📖	mathematical	—	Continuous	—	—

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div' 📖	—	ContinuousOn	—	—	ContinuousWithinAt.div'
inv 📖	—	ContinuousOn	—	—	ContinuousWithinAt.inv
neg 📖	—	ContinuousOn	—	—	ContinuousWithinAt.neg
sub 📖	—	ContinuousOn	—	—	ContinuousWithinAt.sub

ContinuousSub

Theorems

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

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div' 📖	—	ContinuousWithinAt	—	—	Filter.Tendsto.div'
inv 📖	—	ContinuousWithinAt	—	—	Filter.Tendsto.inv
neg 📖	—	ContinuousWithinAt	—	—	Filter.Tendsto.neg
sub 📖	—	ContinuousWithinAt	—	—	Filter.Tendsto.sub

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div' 📖	—	Filter.Tendsto nhds	—	—	comp Continuous.tendsto ContinuousDiv.continuous_div' prodMk_nhds
inv 📖	—	Filter.Tendsto nhds	—	—	comp Continuous.tendsto ContinuousInv.continuous_inv
neg 📖	—	Filter.Tendsto nhds	—	—	comp Continuous.tendsto ContinuousNeg.continuous_neg
sub 📖	—	Filter.Tendsto nhds	—	—	comp Continuous.tendsto ContinuousSub.continuous_sub prodMk_nhds

IsTopologicalAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContinuousAdd 📖	mathematical	—	ContinuousAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
toContinuousNeg 📖	mathematical	—	ContinuousNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
to_continuousSub 📖	mathematical	—	ContinuousSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg Continuous.comp₂ continuous_add toContinuousAdd continuous_fst Continuous.comp ContinuousNeg.continuous_neg toContinuousNeg continuous_snd

IsTopologicalGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContinuousInv 📖	mathematical	—	ContinuousInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
toContinuousMul 📖	mathematical	—	ContinuousMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
to_continuousDiv 📖	mathematical	—	ContinuousDiv DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv Continuous.comp₂ continuous_mul toContinuousMul continuous_fst Continuous.comp ContinuousInv.continuous_inv toContinuousInv continuous_snd

(root)

Definitions

Name	Category	Theorems
ContinuousDiv 📖	CompData	2 math math: IsTopologicalGroup.to_continuousDiv, SeparationQuotient.instContinuousDiv
ContinuousInv 📖	CompData	16 math math: SeparationQuotient.instContinuousInv, instContinuousInvMultiplicativeOfContinuousNeg, Pi.has_continuous_inv', continuousInv_inf, ENNReal.instContinuousInv, continuousInv_of_discreteTopology, Prod.continuousInv, ContinuousInv.induced, OrderDual.instContinuousInv, IsTopologicalGroup.toContinuousInv, instContinuousInvULift, instContinuousInvMulOpposite, instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar, Topology.IsInducing.continuousInv, ContinuousInv.of_nhds_one, CategoryTheory.PreGaloisCategory.instContinuousInvAutFunctorFintypeCat
ContinuousNeg 📖	CompData	26 math math: TrivSqZeroExt.instContinuousNeg, SeparationQuotient.instContinuousNeg, Pi.has_continuous_neg', instContinuousNegElemBallOfNat, continuousNeg_inf, OrderDual.instContinuousNeg, IsTopologicalAddGroup.toContinuousNeg, instContinuousNegElemSphereOfNat, instContinuousNegMulOpposite, instContinuousNegElemClosedBallOfNat, ContinuousNeg.of_nhds_zero, IsModuleTopology.continuousNeg, ContinuousMapZero.instContinuousNeg, instContinuousNegMatrix, IsTopologicalRing.toContinuousNeg, instContinuousNegAddOpposite, ContinuousNeg.of_continuousConstSMul, IsTopologicalSemiring.continuousNeg_of_mul, instContinuousNegULift, Prod.continuousNeg, continuousNeg_of_discreteTopology, EReal.instContinuousNeg, ContinuousNeg.induced, ContinuousLinearMapWOT.instContinuousNeg, Topology.IsInducing.continuousNeg, instContinuousNegAdditiveOfContinuousInv
ContinuousSub 📖	CompData	4 math math: NNRat.instContinuousSub, IsTopologicalAddGroup.to_continuousSub, NNReal.instContinuousSub, SeparationQuotient.instContinuousSub
IsTopologicalAddGroup 📖	CompData	53 math math: IsLeftUniformAddGroup.toIsTopologicalAddGroup, WeakSpace.instIsTopologicalAddGroup, ContinuousLinearMap.topologicalAddGroup, Prod.instIsTopologicalAddGroup, ContDiffMapSupportedIn.isTopologicalAddGroup, topologicalAddGroup_inf, IsTopologicalAddGroup.of_comm_of_nhds_zero, IsValuativeTopology.isTopologicalAddGroup, TestFunction.instIsTopologicalAddGroup, AddGroupFilterBasis.isTopologicalAddGroup, Topology.IsInducing.topologicalAddGroup, ContinuousAlternatingMap.instIsTopologicalAddGroup, ContinuousMap.instIsTopologicalAddGroup, IsModuleTopology.topologicalAddGroup, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, QuotientAddGroup.instIsTopologicalAddGroup, ContinuousLinearMapWOT.instIsTopologicalAddGroup, WeakDual.instIsTopologicalAddGroup, CStarMatrix.instIsTopologicalAddGroup, IsUniformAddGroup.to_topologicalAddGroup, instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup, OrderDual.instIsTopologicalAddGroup, topologicalAddGroup_induced, NonarchimedeanAddGroup.toIsTopologicalAddGroup, AddSubgroup.instIsTopologicalAddGroupSubtypeMem, instIsTopologicalAddGroupAddOpposite, IsTopologicalAddGroup.of_nhds_zero, AddGroupTopology.toIsTopologicalAddGroup, instIsTopologicalAddGroupMatrix, TopModuleCat.isTopologicalAddGroup, topologicalAddGroup_of_discreteTopology, Submodule.topologicalAddGroup_quotient, UniformConvergenceCLM.instIsTopologicalAddGroup, ContinuousAddMonoidHom.instIsTopologicalAddGroup, TopModuleCat.instIsTopologicalAddGroupCarrier, topologicalAddGroup_of_lieAddGroup, AddUnits.instIsTopologicalAddGroupOfContinuousAdd, IsRightUniformAddGroup.toIsTopologicalAddGroup, Submodule.topologicalAddGroup, instIsTopologicalAddGroupReal, WithIdealFilter.instIsTopologicalAddGroup, IsTopologicalAddTorsor.to_isTopologicalAddGroup, IsTopologicalAddGroup.of_nhds_zero', SeminormedAddCommGroup.toIsTopologicalAddGroup, IsTopologicalRing.to_topologicalAddGroup, SchwartzMap.instIsTopologicalAddGroup, Rat.instIsTopologicalAddGroup, ContinuousMultilinearMap.instIsTopologicalAddGroup, WeakBilin.instIsTopologicalAddGroup, ProfiniteAddGrp.topologicalAddGroup, WithSeminorms.topologicalAddGroup, LinearOrderedAddCommGroup.toIsTopologicalAddGroup, SeparationQuotient.instIsTopologicalAddGroup
IsTopologicalGroup 📖	CompData	35 math math: ContinuousMap.instIsTopologicalGroup, IsUniformGroup.to_topologicalGroup, ContinuousMonoidHom.instIsTopologicalGroup, OrderDual.instIsTopologicalGroup, Matrix.SpecialLinearGroup.topologicalGroup, SeparationQuotient.instIsTopologicalGroup, topologicalGroup_of_discreteTopology, IsTopologicalGroup.of_comm_of_nhds_one, instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup, topologicalGroup_inf, NonarchimedeanGroup.toIsTopologicalGroup, instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar, Units.instIsTopologicalGroupOfContinuousMul, IsTopologicalGroup.of_nhds_one, Subgroup.instIsTopologicalGroupSubtypeMem, ProfiniteGrp.topologicalGroup, Circle.instIsTopologicalGroup, IsRightUniformGroup.toIsTopologicalGroup, instIsTopologicalGroupMulOpposite, topologicalGroup_of_lieGroup, GroupFilterBasis.isTopologicalGroup, instIsTopologicalGroupAlgEquiv, GroupTopology.toIsTopologicalGroup, topologicalGroup_induced, IsTopologicalGroup.of_nhds_one', instIsTopologicalGroupULift, LinearOrderedCommGroup.toIsTopologicalGroup, Prod.instIsTopologicalGroup, CategoryTheory.PreGaloisCategory.instIsTopologicalGroupAutFunctorFintypeCat, Topology.IsInducing.topologicalGroup, QuotientGroup.instIsTopologicalGroup, SeminormedCommGroup.toIsTopologicalGroup, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, IsLeftUniformGroup.toIsTopologicalGroup, Metric.sphere.instIsTopologicalGroup

---

← Back to Index