Theorems · Inductive type · general topology

ContinuousConstVAdd

(Γ : Type u_1) → (T : Type u_2) → [TopologicalSpace T] → [VAdd Γ T] → Prop

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

Cited by

97 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

TopologicalSpaceVAdd