Structures · Topology
ContinuousInv
Basic hypothesis to talk about a topological group. A topological group over M, for example,
is obtained by requiring the instances Group M and ContinuousMul M and
ContinuousInv M.
- Defined in
- Mathlib.Topology.Algebra.Group.Defs
- Shape
- One type argument · adds continuous_inv
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances10
- SeparationQuotient
- ENNReal
- RestrictedProduct
- CategoryTheory.Aut
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by104
- ContinuousInv.continuous_inv
- Homeomorph.inv
- Continuous.fun_inv
- Filter.Tendsto.inv
- MeasureTheory.StronglyMeasurable.inv
- tendsto_inv_iff
- IsClosed.smul_left_of_isCompact
- IsOpen.inv
- MeasureTheory.AEStronglyMeasurable.inv
- IsCompact.inv
- Continuous.inv
- Path.inv
- IsClosed.inv
- inv_closure
- ContinuousAt.inv
- ContinuousWithinAt.inv
- tendsto_inv_nhdsGT
- tendsto_inv_nhdsLE_inv
- tendsto_inv_nhdsLE
- isOpenMap_inv
- tendsto_inv_nhdsLT
- Filter.Tendsto.den
- MeasureTheory.IsStronglyProgressive.inv
- ergodic_smul_of_denseRange_zpow
- toUnits_homeomorph
- Specializes.inv
- aeconst_of_dense_aestabilizer_smul
- continuousAt_inv_iff
- tendsto_inv_nhdsGE
- Continuous.of_coeHom_comp
- continuous_inv_iff
- Specializes.zpow
- Topology.IsInducing.continuousInv
- ContinuousOn.inv
- continuousOn_inv_iff
- continuousAt_inv
- MeasureTheory.AEStronglyMeasurable.fun_inv
- isClosed_setOfPred_map_inv
- Inseparable.zpow
- Joined.inv
- instContinuousNegAdditiveOfContinuousInv
- continuousWithinAt_inv
- IsTopologicalGroup.continuous_conj_prod
- SeparationQuotient.instContinuousInv
- ContinuousMap.inv_apply
- Units.isEmbedding_val
- continuousOn_inv
- tendsto_inv_nhdsGE_inv
- MulAction.isClosedMap_quotient
- tendsto_inv_nhdsGT_inv
Ancestors0
No ancestors.