Structures · Topology
ContinuousNeg
Basic hypothesis to talk about a topological additive group. A topological additive group
over M, for example, is obtained by requiring the instances AddGroup M and
ContinuousAdd M and ContinuousNeg M.
- Defined in
- Mathlib.Topology.Algebra.Group.Defs
- Shape
- One type argument · adds continuous_neg
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Concrete types that are instances14
- SeparationQuotient
- Matrix
- EReal
- RestrictedProduct
- TrivSqZeroExt
- ContinuousMapZero
- Circle
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- AddOpposite
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by134
- ContinuousNeg.continuous_neg
- Filter.Tendsto.neg
- Homeomorph.neg
- Continuous.fun_neg
- ContinuousOn.neg
- ContinuousOn.fun_neg
- MeasureTheory.AEStronglyMeasurable.neg
- ContinuousLinearEquiv.neg
- Continuous.neg
- MeasureTheory.StronglyMeasurable.neg
- ContinuousWithinAt.neg
- IsCompact.neg
- ContinuousAt.neg
- MeasureTheory.StronglyAdapted.neg
- IsClosed.vadd_left_of_isCompact
- IsOpen.neg
- ContinuousAt.fun_neg
- Asymptotics.IsBigOTVS.neg_left
- continuousAt_neg
- ContinuousLinearEquiv.neg_apply
- Path.neg
- Asymptotics.IsLittleOTVS.neg_left
- tendsto_neg_nhdsLT
- Asymptotics.IsLittleOTVS.symm
- Asymptotics.IsBigOTVS.neg_right
- continuousWithinAt_neg
- neg_closure
- tendsto_neg_nhdsGT_neg
- IsClosed.neg
- Asymptotics.IsBigOTVS.symm
- Asymptotics.isBigOTVS_neg_right
- toAddUnits_homeomorph
- isOpenMap_neg
- continuous_neg_iff
- MeasureTheory.IsStronglyProgressive.neg
- Flow.reverse
- isClosed_setOfPred_map_neg
- Asymptotics.isLittleOTVS_neg_right
- IsCompactOperator.neg
- ergodic_vadd_of_denseRange_zsmul
- Topology.IsInducing.continuousNeg
- continuousOn_neg_iff
- Measurable.sub_stronglyMeasurable
- Asymptotics.isBigOTVS_comm
- Asymptotics.isLittleOTVS_neg_left
- Asymptotics.isBigOTVS_neg_left
- nhds_neg
- Asymptotics.IsLittleOTVS.neg_right
- Specializes.zsmul
- Asymptotics.isLittleOTVS_comm
Ancestors0
No ancestors.