mathlib documentation

topology.algebra.mul_action

Continuous monoid action #

In this file we define class has_continuous_smul. We say has_continuous_smul M X if M acts on X and the map (c, x) ↦ c • x is continuous on M × X. We reuse this class for topological (semi)modules, vector spaces and algebras.

Main definitions #

Main results #

Besides homeomorphisms mentioned above, in this file we provide lemmas like continuous.smul or filter.tendsto.smul that provide dot-syntax access to continuous_smul.

@[class]
structure has_continuous_vadd (M : Type u_1) (X : Type u_2) [has_vadd M X] [topological_space M] [topological_space X] :
Prop

Class has_continuous_vadd 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.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem filter.tendsto.vadd {M : Type u_1} {X : Type u_2} {α : Type u_4} [topological_space M] [topological_space X] [has_vadd M X] [has_continuous_vadd M X] {f : α → M} {g : α → X} {l : filter α} {c : M} {a : X} (hf : filter.tendsto f l (nhds c)) (hg : filter.tendsto g l (nhds a)) :
filter.tendsto (λ (x : α), f x +ᵥ g x) l (nhds (c +ᵥ a))
theorem filter.tendsto.smul {M : Type u_1} {X : Type u_2} {α : Type u_4} [topological_space M] [topological_space X] [has_smul M X] [has_continuous_smul M X] {f : α → M} {g : α → X} {l : filter α} {c : M} {a : X} (hf : filter.tendsto f l (nhds c)) (hg : filter.tendsto g l (nhds a)) :
filter.tendsto (λ (x : α), f x g x) l (nhds (c a))
theorem filter.tendsto.smul_const {M : Type u_1} {X : Type u_2} {α : Type u_4} [topological_space M] [topological_space X] [has_smul M X] [has_continuous_smul M X] {f : α → M} {l : filter α} {c : M} (hf : filter.tendsto f l (nhds c)) (a : X) :
filter.tendsto (λ (x : α), f x a) l (nhds (c a))
theorem filter.tendsto.vadd_const {M : Type u_1} {X : Type u_2} {α : Type u_4} [topological_space M] [topological_space X] [has_vadd M X] [has_continuous_vadd M X] {f : α → M} {l : filter α} {c : M} (hf : filter.tendsto f l (nhds c)) (a : X) :
filter.tendsto (λ (x : α), f x +ᵥ a) l (nhds (c +ᵥ a))
theorem continuous_within_at.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_smul M X] [has_continuous_smul M X] {f : Y → M} {g : Y → X} {b : Y} {s : set Y} (hf : continuous_within_at f s b) (hg : continuous_within_at g s b) :
continuous_within_at (λ (x : Y), f x g x) s b
theorem continuous_within_at.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_vadd M X] [has_continuous_vadd M X] {f : Y → M} {g : Y → X} {b : Y} {s : set Y} (hf : continuous_within_at f s b) (hg : continuous_within_at g s b) :
continuous_within_at (λ (x : Y), f x +ᵥ g x) s b
theorem continuous_at.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_smul M X] [has_continuous_smul M X] {f : Y → M} {g : Y → X} {b : Y} (hf : continuous_at f b) (hg : continuous_at g b) :
continuous_at (λ (x : Y), f x g x) b
theorem continuous_at.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_vadd M X] [has_continuous_vadd M X] {f : Y → M} {g : Y → X} {b : Y} (hf : continuous_at f b) (hg : continuous_at g b) :
continuous_at (λ (x : Y), f x +ᵥ g x) b
theorem continuous_on.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_vadd M X] [has_continuous_vadd M X] {f : Y → M} {g : Y → X} {s : set Y} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : Y), f x +ᵥ g x) s
theorem continuous_on.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_smul M X] [has_continuous_smul M X] {f : Y → M} {g : Y → X} {s : set Y} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : Y), f x g x) s
@[continuity]
theorem continuous.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_smul M X] [has_continuous_smul M X] {f : Y → M} {g : Y → X} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : Y), f x g x)
@[continuity]
theorem continuous.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_vadd M X] [has_continuous_vadd M X] {f : Y → M} {g : Y → X} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : Y), f x +ᵥ g x)
@[protected, instance]

If a scalar is central, then its right action is continuous when its left action is.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def prod.has_continuous_smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_smul M X] [has_smul M Y] [has_continuous_smul M X] [has_continuous_smul M Y] :
@[protected, instance]
def prod.has_continuous_vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [topological_space M] [topological_space X] [topological_space Y] [has_vadd M X] [has_vadd M Y] [has_continuous_vadd M X] [has_continuous_vadd M Y] :
@[protected, instance]
def pi.has_continuous_vadd {M : Type u_1} [topological_space M] {ι : Type u_2} {γ : ι → Type u_3} [Π (i : ι), topological_space (γ i)] [Π (i : ι), has_vadd M (γ i)] [∀ (i : ι), has_continuous_vadd M (γ i)] :
has_continuous_vadd M (Π (i : ι), γ i)
@[protected, instance]
def pi.has_continuous_smul {M : Type u_1} [topological_space M] {ι : Type u_2} {γ : ι → Type u_3} [Π (i : ι), topological_space (γ i)] [Π (i : ι), has_smul M (γ i)] [∀ (i : ι), has_continuous_smul M (γ i)] :
has_continuous_smul M (Π (i : ι), γ i)
theorem has_continuous_vadd_Inf {M : Type u_2} {X : Type u_3} [topological_space M] [has_vadd M X] {ts : set (topological_space X)} (h : ∀ (t : topological_space X), t tshas_continuous_vadd M X) :
theorem has_continuous_smul_Inf {M : Type u_2} {X : Type u_3} [topological_space M] [has_smul M X] {ts : set (topological_space X)} (h : ∀ (t : topological_space X), t tshas_continuous_smul M X) :
theorem has_continuous_vadd_infi {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [topological_space M] [has_vadd M X] {ts' : ι → topological_space X} (h : ∀ (i : ι), has_continuous_vadd M X) :
theorem has_continuous_smul_infi {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [topological_space M] [has_smul M X] {ts' : ι → topological_space X} (h : ∀ (i : ι), has_continuous_smul M X) :
theorem has_continuous_vadd_inf {M : Type u_2} {X : Type u_3} [topological_space M] [has_vadd M X] {t₁ t₂ : topological_space X} [has_continuous_vadd M X] [has_continuous_vadd M X] :
theorem has_continuous_smul_inf {M : Type u_2} {X : Type u_3} [topological_space M] [has_smul M X] {t₁ t₂ : topological_space X} [has_continuous_smul M X] [has_continuous_smul M X] :