Structures · Topology
ContinuousVAdd
Class ContinuousVAdd M X says that the additive action (+ᵥ) : M → X → X
is continuous in both arguments. We use the same class for all kinds of additive actions,
including (semi)modules and algebras.
- Defined in
- Mathlib.Topology.Algebra.MulAction
- Shape
- 2 explicit arguments · adds continuous_vadd
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances6
- DomAddAct
- AddUnits
- Subtype
- OrderDual
- ULift
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by66
- ContinuousVAdd.continuous_vadd
- Continuous.fun_vadd
- ContinuousAffineMap.lineMap
- Continuous.vadd
- Filter.Tendsto.vadd
- IsClosed.vadd_left_of_isCompact
- AddTorsor.connectedSpace
- aeconst_of_dense_setOfPred_preimage_vadd_ae
- aeconst_of_dense_setOfPred_preimage_vadd_eq
- vadd_set_closure_subset
- ContinuousWithinAt.vadd
- AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty
- IsCompact.vadd_set
- ContinuousOn.vadd
- ContinuousAffineMap.lineMap_toAffineMap
- MeasureTheory.AEStronglyMeasurable.vadd
- ContinuousAt.vadd
- isOpenMap_vadd_of_sigmaCompact
- ergodic_vadd_of_denseRange_zsmul
- AddAction.continuousVAdd_compHom
- ContinuousOn.fun_vadd
- Filter.Tendsto.zero_vadd
- ergodic_vadd_of_denseRange_nsmul
- MeasureTheory.StronglyMeasurable.vadd
- Specializes.vadd
- Inseparable.vadd
- aeconst_of_dense_aestabilizer_vadd
- vadd_singleton_mem_nhds_of_sigmaCompact
- Filter.Tendsto.vadd_const
- ContinuousAffineMap.coe_lineMap_eq
- ContinuousVAdd.continuousConstVAdd
- AddAction.properVAdd_of_proper_orbitMap
- AddOpposite.continuousVAdd
- AddUnits.continuousVAdd
- AddSubgroup.continuousVAdd
- ContinuousWithinAt.fun_vadd
- MeasureTheory.StronglyMeasurable.vadd_const
- ContinuousMap.instContinuousVAdd
- MeasureTheory.Lp.instContinuousVAddDomAddAct
- OrderDual.instContinuousVAdd_left
- aeconst_of_dense_setOf_preimage_vadd_eq
- OrderDual.instContinuousVAdd_right
- MeasureTheory.AEStronglyMeasurable.fun_vadd
- instContMDiffVAddOfNatWithTopENatOfContinuousVAdd
- AddAction.isClosedMap_quotient
- RestrictedProduct.continuousVAdd
- MeasureTheory.StronglyMeasurable.fun_vadd
- instContinuousVAddForall
- AddSubmonoid.continuousVAdd
- continuousVAdd_inf
Ancestors0
No ancestors.