Documentation

Mathlib.Topology.Algebra.ConstMulAction

Monoid actions continuous in the second variable #

In this file we define class ContinuousConstSMul. We say ContinuousConstSMul Γ T if Γ acts on T and for each γ, the map x ↦ γ • x is continuous. (This differs from ContinuousSMul, which requires simultaneous continuity in both variables.)

Main definitions #

Main results #

Tags #

Hausdorff, discrete group, properly discontinuous, quotient space

class ContinuousConstSMul (Γ : Type u_1) (T : Type u_2) [TopologicalSpace T] [SMul Γ T] :

Class ContinuousConstSMul Γ T says that the scalar multiplication (•) : Γ → T → T is continuous in the second argument. We use the same class for all kinds of multiplicative actions, including (semi)modules and algebras.

Note that both ContinuousConstSMul α α and ContinuousConstSMul αᵐᵒᵖ α are weaker versions of ContinuousMul α.

  • continuous_const_smul : ∀ (γ : Γ), Continuous fun (x : T) => γ x

    The scalar multiplication (•) : Γ → T → T is continuous in the second argument.

Instances
theorem ContinuousConstSMul.continuous_const_smul {Γ : Type u_1} {T : Type u_2} [TopologicalSpace T] [SMul Γ T] [self : ContinuousConstSMul Γ T] (γ : Γ) :
Continuous fun (x : T) => γ x

The scalar multiplication (•) : Γ → T → T is continuous in the second argument.

class ContinuousConstVAdd (Γ : Type u_1) (T : Type u_2) [TopologicalSpace T] [VAdd Γ T] :

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 α.

  • continuous_const_vadd : ∀ (γ : Γ), Continuous fun (x : T) => γ +ᵥ x

    The additive action (+ᵥ) : Γ → T → T is continuous in the second argument.

Instances
theorem ContinuousConstVAdd.continuous_const_vadd {Γ : Type u_1} {T : Type u_2} [TopologicalSpace T] [VAdd Γ T] [self : ContinuousConstVAdd Γ T] (γ : Γ) :
Continuous fun (x : T) => γ +ᵥ x

The additive action (+ᵥ) : Γ → T → T is continuous in the second argument.

Equations
  • =
Equations
  • =
theorem Filter.Tendsto.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {f : βα} {l : Filter β} {a : α} (hf : Filter.Tendsto f l (nhds a)) (c : M) :
Filter.Tendsto (fun (x : β) => c +ᵥ f x) l (nhds (c +ᵥ a))
theorem Filter.Tendsto.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {f : βα} {l : Filter β} {a : α} (hf : Filter.Tendsto f l (nhds a)) (c : M) :
Filter.Tendsto (fun (x : β) => c f x) l (nhds (c a))
theorem ContinuousWithinAt.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] [TopologicalSpace β] {g : βα} {b : β} {s : Set β} (hg : ContinuousWithinAt g s b) (c : M) :
ContinuousWithinAt (fun (x : β) => c +ᵥ g x) s b
theorem ContinuousWithinAt.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] [TopologicalSpace β] {g : βα} {b : β} {s : Set β} (hg : ContinuousWithinAt g s b) (c : M) :
ContinuousWithinAt (fun (x : β) => c g x) s b
theorem ContinuousAt.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] [TopologicalSpace β] {g : βα} {b : β} (hg : ContinuousAt g b) (c : M) :
ContinuousAt (fun (x : β) => c +ᵥ g x) b
theorem ContinuousAt.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] [TopologicalSpace β] {g : βα} {b : β} (hg : ContinuousAt g b) (c : M) :
ContinuousAt (fun (x : β) => c g x) b
theorem ContinuousOn.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] [TopologicalSpace β] {g : βα} {s : Set β} (hg : ContinuousOn g s) (c : M) :
ContinuousOn (fun (x : β) => c +ᵥ g x) s
theorem ContinuousOn.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] [TopologicalSpace β] {g : βα} {s : Set β} (hg : ContinuousOn g s) (c : M) :
ContinuousOn (fun (x : β) => c g x) s
theorem Continuous.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] [TopologicalSpace β] {g : βα} (hg : Continuous g) (c : M) :
Continuous fun (x : β) => c +ᵥ g x
theorem Continuous.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] [TopologicalSpace β] {g : βα} (hg : Continuous g) (c : M) :
Continuous fun (x : β) => c g x

If an additive action is central, then its right action is continuous when its left action is.

Equations
  • =

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

Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • = inst
Equations
  • = inst
Equations
  • = inst
Equations
  • = inst
instance Prod.continuousConstVAdd {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] [TopologicalSpace β] [VAdd M β] [ContinuousConstVAdd M β] :
Equations
  • =
instance Prod.continuousConstSMul {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] [TopologicalSpace β] [SMul M β] [ContinuousConstSMul M β] :
Equations
  • =
instance instContinuousConstVAddForall {M : Type u_1} {ι : Type u_4} {γ : ιType u_5} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → VAdd M (γ i)] [∀ (i : ι), ContinuousConstVAdd M (γ i)] :
ContinuousConstVAdd M ((i : ι) → γ i)
Equations
  • =
instance instContinuousConstSMulForall {M : Type u_1} {ι : Type u_4} {γ : ιType u_5} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → SMul M (γ i)] [∀ (i : ι), ContinuousConstSMul M (γ i)] :
ContinuousConstSMul M ((i : ι) → γ i)
Equations
  • =
theorem IsCompact.vadd {α : Type u_4} {β : Type u_5} [VAdd α β] [TopologicalSpace β] [ContinuousConstVAdd α β] (a : α) {s : Set β} (hs : IsCompact s) :
theorem IsCompact.smul {α : Type u_4} {β : Type u_5} [SMul α β] [TopologicalSpace β] [ContinuousConstSMul α β] (a : α) {s : Set β} (hs : IsCompact s) :
theorem Specializes.const_vadd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {x : α} {y : α} (h : x y) (c : M) :
(c +ᵥ x) (c +ᵥ y)
theorem Specializes.const_smul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {x : α} {y : α} (h : x y) (c : M) :
(c x) (c y)
theorem Inseparable.const_vadd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {x : α} {y : α} (h : Inseparable x y) (c : M) :
Inseparable (c +ᵥ x) (c +ᵥ y)
theorem Inseparable.const_smul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {x : α} {y : α} (h : Inseparable x y) (c : M) :
Inseparable (c x) (c y)
theorem Inducing.continuousConstVAdd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {N : Type u_4} {β : Type u_5} [VAdd N β] [TopologicalSpace β] {g : βα} (hg : Inducing g) (f : NM) (hf : ∀ {c : N} {x : β}, g (c +ᵥ x) = f c +ᵥ g x) :
theorem Inducing.continuousConstSMul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {N : Type u_4} {β : Type u_5} [SMul N β] [TopologicalSpace β] {g : βα} (hg : Inducing g) (f : NM) (hf : ∀ {c : N} {x : β}, g (c x) = f c g x) :
Equations
  • =
Equations
  • =
theorem vadd_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [ContinuousConstVAdd M α] (c : M) (s : Set α) :
theorem smul_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [ContinuousConstSMul M α] (c : M) (s : Set α) :
theorem vadd_closure_orbit_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [ContinuousConstVAdd M α] (c : M) (x : α) :
theorem smul_closure_orbit_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [ContinuousConstSMul M α] (c : M) (x : α) :
theorem isClosed_setOf_map_smul {M : Type u_1} [Monoid M] {N : Type u_4} [Monoid N] (α : Type u_5) (β : Type u_6) [MulAction M α] [MulAction N β] [TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β] (σ : MN) :
IsClosed {f : αβ | ∀ (c : M) (x : α), f (c x) = σ c f x}
theorem tendsto_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {f : βα} {l : Filter β} {a : α} (c : G) :
Filter.Tendsto (fun (x : β) => c +ᵥ f x) l (nhds (c +ᵥ a)) Filter.Tendsto f l (nhds a)
theorem tendsto_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {f : βα} {l : Filter β} {a : α} (c : G) :
Filter.Tendsto (fun (x : β) => c f x) l (nhds (c a)) Filter.Tendsto f l (nhds a)
theorem continuousWithinAt_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] [TopologicalSpace β] {f : βα} {b : β} {s : Set β} (c : G) :
ContinuousWithinAt (fun (x : β) => c +ᵥ f x) s b ContinuousWithinAt f s b
theorem continuousWithinAt_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] [TopologicalSpace β] {f : βα} {b : β} {s : Set β} (c : G) :
ContinuousWithinAt (fun (x : β) => c f x) s b ContinuousWithinAt f s b
theorem continuousOn_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] [TopologicalSpace β] {f : βα} {s : Set β} (c : G) :
ContinuousOn (fun (x : β) => c +ᵥ f x) s ContinuousOn f s
theorem continuousOn_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] [TopologicalSpace β] {f : βα} {s : Set β} (c : G) :
ContinuousOn (fun (x : β) => c f x) s ContinuousOn f s
theorem continuousAt_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] [TopologicalSpace β] {f : βα} {b : β} (c : G) :
ContinuousAt (fun (x : β) => c +ᵥ f x) b ContinuousAt f b
theorem continuousAt_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] [TopologicalSpace β] {f : βα} {b : β} (c : G) :
ContinuousAt (fun (x : β) => c f x) b ContinuousAt f b
theorem continuous_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] [TopologicalSpace β] {f : βα} (c : G) :
(Continuous fun (x : β) => c +ᵥ f x) Continuous f
theorem continuous_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] [TopologicalSpace β] {f : βα} (c : G) :
(Continuous fun (x : β) => c f x) Continuous f
theorem Homeomorph.vadd.proof_2 {α : Type u_1} {G : Type u_2} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (γ : G) :
Continuous fun (x : α) => -γ +ᵥ x
def Homeomorph.vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (γ : G) :
α ≃ₜ α

The homeomorphism given by affine-addition by an element of an additive group Γ acting on T is a homeomorphism from T to itself.

Equations
theorem Homeomorph.vadd.proof_1 {α : Type u_1} {G : Type u_2} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (γ : G) :
Continuous fun (x : α) => γ +ᵥ x
@[simp]
theorem Homeomorph.smul_symm_apply {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (γ : G) (x : α) :
(Homeomorph.smul γ).symm x = γ⁻¹ x
@[simp]
theorem Homeomorph.smul_apply {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (γ : G) (x : α) :
(Homeomorph.smul γ) x = γ x
@[simp]
theorem Homeomorph.vadd_apply {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (γ : G) (x : α) :
(Homeomorph.vadd γ) x = γ +ᵥ x
@[simp]
theorem Homeomorph.vadd_symm_apply {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (γ : G) (x : α) :
(Homeomorph.vadd γ).symm x = -γ +ᵥ x
def Homeomorph.smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (γ : G) :
α ≃ₜ α

The homeomorphism given by scalar multiplication by a given element of a group Γ acting on T is a homeomorphism from T to itself.

Equations
theorem isOpenMap_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) :
IsOpenMap fun (x : α) => c +ᵥ x
theorem isOpenMap_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) :
IsOpenMap fun (x : α) => c x
theorem IsOpen.vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {s : Set α} (hs : IsOpen s) (c : G) :
IsOpen (c +ᵥ s)
theorem IsOpen.smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set α} (hs : IsOpen s) (c : G) :
IsOpen (c s)
theorem isClosedMap_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) :
IsClosedMap fun (x : α) => c +ᵥ x
theorem isClosedMap_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) :
IsClosedMap fun (x : α) => c x
theorem IsClosed.vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {s : Set α} (hs : IsClosed s) (c : G) :
theorem IsClosed.smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set α} (hs : IsClosed s) (c : G) :
theorem closure_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) (s : Set α) :
theorem closure_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) (s : Set α) :
closure (c s) = c closure s
theorem Dense.vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) {s : Set α} (hs : Dense s) :
Dense (c +ᵥ s)
theorem Dense.smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) {s : Set α} (hs : Dense s) :
Dense (c s)
theorem interior_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) (s : Set α) :
theorem interior_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) (s : Set α) :
theorem IsOpen.vadd_left {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {s : Set G} {t : Set α} (ht : IsOpen t) :
IsOpen (s +ᵥ t)
theorem IsOpen.smul_left {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set G} {t : Set α} (ht : IsOpen t) :
IsOpen (s t)
theorem subset_interior_vadd_right {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {s : Set G} {t : Set α} :
theorem subset_interior_smul_right {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set G} {t : Set α} :
@[simp]
theorem vadd_mem_nhds_vadd_iff {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {t : Set α} (g : G) {a : α} :
g +ᵥ t nhds (g +ᵥ a) t nhds a
@[simp]
theorem smul_mem_nhds_smul_iff {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {t : Set α} (g : G) {a : α} :
g t nhds (g a) t nhds a
theorem smul_mem_nhds_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {t : Set α} (g : G) {a : α} :
t nhds ag t nhds (g a)

Alias of the reverse direction of smul_mem_nhds_smul_iff.

theorem vadd_mem_nhds_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {t : Set α} (g : G) {a : α} :
t nhds ag +ᵥ t nhds (g +ᵥ a)
@[deprecated]
theorem smul_mem_nhds {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {t : Set α} (g : G) {a : α} :
t nhds ag t nhds (g a)

Alias of the reverse direction of smul_mem_nhds_smul_iff.


Alias of the reverse direction of smul_mem_nhds_smul_iff.

@[deprecated]
theorem vadd_mem_nhds {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {t : Set α} (g : G) {a : α} :
t nhds ag +ᵥ t nhds (g +ᵥ a)
@[simp]
theorem vadd_mem_nhds_self {G : Type u_4} [AddGroup G] [TopologicalSpace G] [ContinuousConstVAdd G G] {g : G} {s : Set G} :
g +ᵥ s nhds g s nhds 0
@[simp]
theorem smul_mem_nhds_self {G : Type u_4} [Group G] [TopologicalSpace G] [ContinuousConstSMul G G] {g : G} {s : Set G} :
g s nhds g s nhds 1
theorem tendsto_const_smul_iff₀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {f : βα} {l : Filter β} {a : α} {c : G₀} (hc : c 0) :
Filter.Tendsto (fun (x : β) => c f x) l (nhds (c a)) Filter.Tendsto f l (nhds a)
theorem continuousWithinAt_const_smul_iff₀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] [TopologicalSpace β] {f : βα} {b : β} {c : G₀} {s : Set β} (hc : c 0) :
ContinuousWithinAt (fun (x : β) => c f x) s b ContinuousWithinAt f s b
theorem continuousOn_const_smul_iff₀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] [TopologicalSpace β] {f : βα} {c : G₀} {s : Set β} (hc : c 0) :
ContinuousOn (fun (x : β) => c f x) s ContinuousOn f s
theorem continuousAt_const_smul_iff₀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] [TopologicalSpace β] {f : βα} {b : β} {c : G₀} (hc : c 0) :
ContinuousAt (fun (x : β) => c f x) b ContinuousAt f b
theorem continuous_const_smul_iff₀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] [TopologicalSpace β] {f : βα} {c : G₀} (hc : c 0) :
(Continuous fun (x : β) => c f x) Continuous f
@[simp]
theorem Homeomorph.smulOfNeZero_apply {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] (c : G₀) (hc : c 0) :
(Homeomorph.smulOfNeZero c hc) = fun (x : α) => c x
def Homeomorph.smulOfNeZero {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] (c : G₀) (hc : c 0) :
α ≃ₜ α

Scalar multiplication by a non-zero element of a group with zero acting on α is a homeomorphism from α onto itself.

Equations
@[simp]
theorem Homeomorph.smulOfNeZero_symm_apply {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} (hc : c 0) :
(Homeomorph.smulOfNeZero c hc).symm = fun (x : α) => c⁻¹ x
theorem isOpenMap_smul₀ {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} (hc : c 0) :
IsOpenMap fun (x : α) => c x
theorem IsOpen.smul₀ {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} (hs : IsOpen s) (hc : c 0) :
IsOpen (c s)
theorem interior_smul₀ {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} (hc : c 0) (s : Set α) :
theorem closure_smul₀' {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} (hc : c 0) (s : Set α) :
closure (c s) = c closure s
theorem closure_smul₀ {G₀ : Type u_4} [GroupWithZero G₀] {E : Type u_5} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) (s : Set E) :
closure (c s) = c closure s
theorem isClosedMap_smul_of_ne_zero {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} (hc : c 0) :
IsClosedMap fun (x : α) => c x

smul is a closed map in the second argument.

The lemma that smul is a closed map in the first argument (for a normed space over a complete normed field) is isClosedMap_smul_left in Analysis.Normed.Module.FiniteDimension.

theorem IsClosed.smul_of_ne_zero {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} (hs : IsClosed s) (hc : c 0) :
theorem isClosedMap_smul₀ {G₀ : Type u_4} [GroupWithZero G₀] {E : Type u_5} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) :
IsClosedMap fun (x : E) => c x

smul is a closed map in the second argument.

The lemma that smul is a closed map in the first argument (for a normed space over a complete normed field) is isClosedMap_smul_left in Analysis.Normed.Module.FiniteDimension.

theorem IsClosed.smul₀ {G₀ : Type u_4} [GroupWithZero G₀] {E : Type u_5} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) {s : Set E} (hs : IsClosed s) :
theorem HasCompactMulSupport.comp_smul {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {β : Type u_5} [One β] {f : αβ} (h : HasCompactMulSupport f) {c : G₀} (hc : c 0) :
HasCompactMulSupport fun (x : α) => f (c x)
theorem HasCompactSupport.comp_smul {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {β : Type u_5} [Zero β] {f : αβ} (h : HasCompactSupport f) {c : G₀} (hc : c 0) :
HasCompactSupport fun (x : α) => f (c x)
theorem IsUnit.tendsto_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] {f : βα} {l : Filter β} {a : α} {c : M} (hc : IsUnit c) :
Filter.Tendsto (fun (x : β) => c f x) l (nhds (c a)) Filter.Tendsto f l (nhds a)
theorem IsUnit.continuousWithinAt_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] [TopologicalSpace β] {f : βα} {b : β} {c : M} {s : Set β} (hc : IsUnit c) :
ContinuousWithinAt (fun (x : β) => c f x) s b ContinuousWithinAt f s b
theorem IsUnit.continuousOn_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] [TopologicalSpace β] {f : βα} {c : M} {s : Set β} (hc : IsUnit c) :
ContinuousOn (fun (x : β) => c f x) s ContinuousOn f s
theorem IsUnit.continuousAt_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] [TopologicalSpace β] {f : βα} {b : β} {c : M} (hc : IsUnit c) :
ContinuousAt (fun (x : β) => c f x) b ContinuousAt f b
theorem IsUnit.continuous_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] [TopologicalSpace β] {f : βα} {c : M} (hc : IsUnit c) :
(Continuous fun (x : β) => c f x) Continuous f
theorem IsUnit.isOpenMap_smul {M : Type u_1} {α : Type u_2} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] {c : M} (hc : IsUnit c) :
IsOpenMap fun (x : α) => c x
theorem IsUnit.isClosedMap_smul {M : Type u_1} {α : Type u_2} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] {c : M} (hc : IsUnit c) :
IsClosedMap fun (x : α) => c x
theorem IsUnit.smul_mem_nhds_smul_iff {M : Type u_1} {α : Type u_2} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] {c : M} (hc : IsUnit c) {s : Set α} {a : α} :
c s nhds (c a) s nhds a
class ProperlyDiscontinuousSMul (Γ : Type u_4) (T : Type u_5) [TopologicalSpace T] [SMul Γ T] :

Class ProperlyDiscontinuousSMul Γ T says that the scalar multiplication (•) : Γ → T → T is properly discontinuous, that is, for any pair of compact sets K, L in T, only finitely many γ:Γ move K to have nontrivial intersection with L.

  • finite_disjoint_inter_image : ∀ {K L : Set T}, IsCompact KIsCompact L{γ : Γ | (fun (x : T) => γ x) '' K L }.Finite

    Given two compact sets K and L, γ • K ∩ L is nonempty for finitely many γ.

Instances
theorem ProperlyDiscontinuousSMul.finite_disjoint_inter_image {Γ : Type u_4} {T : Type u_5} [TopologicalSpace T] [SMul Γ T] [self : ProperlyDiscontinuousSMul Γ T] {K : Set T} {L : Set T} :
IsCompact KIsCompact L{γ : Γ | (fun (x : T) => γ x) '' K L }.Finite

Given two compact sets K and L, γ • K ∩ L is nonempty for finitely many γ.

class ProperlyDiscontinuousVAdd (Γ : Type u_4) (T : Type u_5) [TopologicalSpace T] [VAdd Γ T] :

Class ProperlyDiscontinuousVAdd Γ T says that the additive action (+ᵥ) : Γ → T → T is properly discontinuous, that is, for any pair of compact sets K, L in T, only finitely many γ:Γ move K to have nontrivial intersection with L.

  • finite_disjoint_inter_image : ∀ {K L : Set T}, IsCompact KIsCompact L{γ : Γ | (fun (x : T) => γ +ᵥ x) '' K L }.Finite

    Given two compact sets K and L, γ +ᵥ K ∩ L is nonempty for finitely many γ.

Instances
theorem ProperlyDiscontinuousVAdd.finite_disjoint_inter_image {Γ : Type u_4} {T : Type u_5} [TopologicalSpace T] [VAdd Γ T] [self : ProperlyDiscontinuousVAdd Γ T] {K : Set T} {L : Set T} :
IsCompact KIsCompact L{γ : Γ | (fun (x : T) => γ +ᵥ x) '' K L }.Finite

Given two compact sets K and L, γ +ᵥ K ∩ L is nonempty for finitely many γ.

@[instance 100]

A finite group action is always properly discontinuous.

Equations
  • =
@[instance 100]

A finite group action is always properly discontinuous.

Equations
  • =
theorem isOpenMap_quotient_mk'_add {Γ : Type u_4} [AddGroup Γ] {T : Type u_5} [TopologicalSpace T] [AddAction Γ T] [ContinuousConstVAdd Γ T] :
IsOpenMap Quotient.mk'

The quotient map by a group action is open, i.e. the quotient by a group action is an open quotient.

theorem isOpenMap_quotient_mk'_mul {Γ : Type u_4} [Group Γ] {T : Type u_5} [TopologicalSpace T] [MulAction Γ T] [ContinuousConstSMul Γ T] :
IsOpenMap Quotient.mk'

The quotient map by a group action is open, i.e. the quotient by a group action is an open quotient.

@[instance 100]

The quotient by a discontinuous group action of a locally compact t2 space is t2.

Equations
  • =
@[instance 100]

The quotient by a discontinuous group action of a locally compact t2 space is t2.

Equations
  • =

The quotient of a second countable space by an additive group action is second countable.

The quotient of a second countable space by a group action is second countable.

theorem smul_mem_nhds_smul_iff₀ {α : Type u_2} {G₀ : Type u_6} [GroupWithZero G₀] [MulAction G₀ α] [TopologicalSpace α] [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} {x : α} (hc : c 0) :
c s nhds (c x) s nhds x

Scalar multiplication by a nonzero scalar preserves neighborhoods.

@[deprecated smul_mem_nhds_smul_iff₀]
theorem set_smul_mem_nhds_smul_iff {α : Type u_2} {G₀ : Type u_6} [GroupWithZero G₀] [MulAction G₀ α] [TopologicalSpace α] [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} {x : α} (hc : c 0) :
c s nhds (c x) s nhds x

Alias of smul_mem_nhds_smul_iff₀.


Scalar multiplication by a nonzero scalar preserves neighborhoods.

theorem smul_mem_nhds_smul₀ {α : Type u_2} {G₀ : Type u_6} [GroupWithZero G₀] [MulAction G₀ α] [TopologicalSpace α] [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} {x : α} (hc : c 0) :
s nhds xc s nhds (c x)

Alias of the reverse direction of smul_mem_nhds_smul_iff₀.


Scalar multiplication by a nonzero scalar preserves neighborhoods.

@[deprecated smul_mem_nhds_smul₀]
theorem set_smul_mem_nhds_smul {α : Type u_2} {G₀ : Type u_6} [GroupWithZero G₀] [MulAction G₀ α] [TopologicalSpace α] [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} {x : α} (hs : s nhds x) (hc : c 0) :
c s nhds (c x)
theorem set_smul_mem_nhds_zero_iff {α : Type u_2} {G₀ : Type u_6} [GroupWithZero G₀] [AddMonoid α] [DistribMulAction G₀ α] [TopologicalSpace α] [ContinuousConstSMul G₀ α] {s : Set α} {c : G₀} (hc : c 0) :
c s nhds 0 s nhds 0