Structures · Topology

ContinuousConstVAdd

Class ContinuousConstVAdd Γ T says that the additive action (+ᵥ) : Γ → T → T is continuous in the second argument. We use the same class for all kinds of additive actions, including (semi)modules and algebras. Note that both ContinuousConstVAdd α α and ContinuousConstVAdd αᵐᵒᵖ α are weaker versions of ContinuousVAdd α.

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Shape

2 explicit arguments · adds continuous_const_vadd