HepLean 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 #

ContinuousConstSMul Γ T : typeclass saying that the map x ↦ γ • x is continuous on T;
ProperlyDiscontinuousSMul: 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.
Homeomorph.smul: scalar multiplication by an element of a group Γ acting on T is a homeomorphism of T.

Main results #

isOpenMap_quotient_mk'_mul : The quotient map by a group action is open.
t2Space_of_properlyDiscontinuousSMul_of_t2Space : The quotient by a discontinuous group action of a locally compact t2 space is t2.

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} :

∀ {inst : TopologicalSpace T} {inst_1 : 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} :

∀ {inst : TopologicalSpace T} {inst_1 : VAdd Γ T} [self : ContinuousConstVAdd Γ T] (γ : Γ), Continuous fun (x : T) => γ +ᵥ x

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

instance instContinuousConstVAddULift {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] :

ContinuousConstVAdd (ULift.{u_4, u_1} M) α

Equations

⋯ = ⋯

instance instContinuousConstSMulULift {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] :

ContinuousConstSMul (ULift.{u_4, u_1} M) α

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

instance ContinuousConstVAdd.op {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] :

ContinuousConstVAdd Mᵃᵒᵖ α

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

Equations

⋯ = ⋯

instance ContinuousConstSMul.op {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] :

ContinuousConstSMul Mᵐᵒᵖ α

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

Equations

⋯ = ⋯

instance AddOpposite.continuousConstVAdd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] :

ContinuousConstVAdd M αᵃᵒᵖ

Equations

⋯ = ⋯

instance MulOpposite.continuousConstSMul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] :

ContinuousConstSMul M αᵐᵒᵖ

Equations

⋯ = ⋯

instance instContinuousConstVAddOrderDual {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] :

ContinuousConstVAdd M αᵒᵈ

Equations

⋯ = inst

instance instContinuousConstSMulOrderDual {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] :

ContinuousConstSMul M αᵒᵈ

Equations

⋯ = inst

instance OrderDual.continuousConstVAdd' {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] :

ContinuousConstVAdd Mᵒᵈ α

Equations

⋯ = inst

instance OrderDual.continuousConstSMul' {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] :

ContinuousConstSMul Mᵒᵈ α

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 β] :

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 β] :

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) :

IsCompact (a +ᵥ s)

theorem IsCompact.smul {α : Type u_4} {β : Type u_5} [SMul α β] [TopologicalSpace β] [ContinuousConstSMul α β] (a : α) {s : Set β} (hs : IsCompact s) :

IsCompact (a • 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 IsInducing.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 : IsInducing g) (f : N → M) (hf : ∀ {c : N} {x : β}, g (c +ᵥ x) = f c +ᵥ g x) :

ContinuousConstVAdd N β

theorem IsInducing.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 : IsInducing g) (f : N → M) (hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x) :

ContinuousConstSMul N β

@[deprecated IsInducing.continuousConstSMul]

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 : IsInducing g) (f : N → M) (hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x) :

ContinuousConstSMul N β

Alias of IsInducing.continuousConstSMul.

instance AddUnits.continuousConstVAdd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [ContinuousConstVAdd M α] :

ContinuousConstVAdd (AddUnits M) α

Equations

⋯ = ⋯

instance Units.continuousConstSMul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [ContinuousConstSMul M α] :

ContinuousConstSMul Mˣ α

Equations

⋯ = ⋯

theorem vadd_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [ContinuousConstVAdd M α] (c : M) (s : Set α) :

c +ᵥ closure s ⊆ closure (c +ᵥ s)

theorem smul_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [ContinuousConstSMul M α] (c : M) (s : Set α) :

c • closure s ⊆ closure (c • s)

theorem vadd_closure_orbit_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [ContinuousConstVAdd M α] (c : M) (x : α) :

c +ᵥ closure (AddAction.orbit M x) ⊆ closure (AddAction.orbit M x)

theorem smul_closure_orbit_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [ContinuousConstSMul M α] (c : M) (x : α) :

c • closure (MulAction.orbit M x) ⊆ closure (MulAction.orbit 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 β] (σ : M → N) :

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

theorem Homeomorph.vadd.proof_1 {α : 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

Homeomorph.vadd γ = { toEquiv := AddAction.toPerm γ, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

@[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.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.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

Homeomorph.smul γ = { toEquiv := MulAction.toPerm γ, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

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) :

IsClosed (c +ᵥ s)

theorem IsClosed.smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set α} (hs : IsClosed s) (c : G) :

IsClosed (c • s)

theorem closure_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) (s : Set α) :

closure (c +ᵥ s) = c +ᵥ closure s

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 α) :

interior (c +ᵥ s) = c +ᵥ interior s

theorem interior_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) (s : Set α) :

interior (c • s) = c • interior s

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 α} :

s +ᵥ interior t ⊆ interior (s +ᵥ t)

theorem subset_interior_smul_right {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set G} {t : Set α} :

s • interior t ⊆ interior (s • t)

@[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 a → g • 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 a → g +ᵥ 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 a → g • 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 a → g +ᵥ 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

Homeomorph.smulOfNeZero c hc = Homeomorph.smul (Units.mk0 c hc)

Instances For

@[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 α) :

interior (c • s) = c • interior s

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) :

IsClosed (c • s)

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) :

IsClosed (c • 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 K → IsCompact 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} :

∀ {inst : TopologicalSpace T} {inst_1 : SMul Γ T} [self : ProperlyDiscontinuousSMul Γ T] {K L : Set T}, IsCompact K → IsCompact 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 K → IsCompact 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} :

∀ {inst : TopologicalSpace T} {inst_1 : VAdd Γ T} [self : ProperlyDiscontinuousVAdd Γ T] {K L : Set T}, IsCompact K → IsCompact L → {γ : Γ | (fun (x : T) => γ +ᵥ x) '' K ∩ L ≠ ∅}.Finite

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

@[instance 100]

instance Finite.to_properlyDiscontinuousVAdd {Γ : Type u_4} [AddGroup Γ] {T : Type u_5} [TopologicalSpace T] [AddAction Γ T] [Finite Γ] :

ProperlyDiscontinuousVAdd Γ T

A finite group action is always properly discontinuous.

Equations

⋯ = ⋯

@[instance 100]

instance Finite.to_properlyDiscontinuousSMul {Γ : Type u_4} [Group Γ] {T : Type u_5} [TopologicalSpace T] [MulAction Γ T] [Finite Γ] :

ProperlyDiscontinuousSMul Γ T

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.

theorem AddAction.isOpenQuotientMap_quotientMk {Γ : Type u_4} [AddGroup Γ] {T : Type u_5} [TopologicalSpace T] [AddAction Γ T] [ContinuousConstVAdd Γ T] :

IsOpenQuotientMap (Quotient.mk (AddAction.orbitRel Γ T))

theorem MulAction.isOpenQuotientMap_quotientMk {Γ : Type u_4} [Group Γ] {T : Type u_5} [TopologicalSpace T] [MulAction Γ T] [ContinuousConstSMul Γ T] :

IsOpenQuotientMap (Quotient.mk (MulAction.orbitRel Γ T))

@[instance 100]

instance t2Space_of_properlyDiscontinuousVAdd_of_t2Space {Γ : Type u_4} [AddGroup Γ] {T : Type u_5} [TopologicalSpace T] [AddAction Γ T] [T2Space T] [LocallyCompactSpace T] [ContinuousConstVAdd Γ T] [ProperlyDiscontinuousVAdd Γ T] :

T2Space (Quotient (AddAction.orbitRel Γ T))

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

Equations

⋯ = ⋯

@[instance 100]

instance t2Space_of_properlyDiscontinuousSMul_of_t2Space {Γ : Type u_4} [Group Γ] {T : Type u_5} [TopologicalSpace T] [MulAction Γ T] [T2Space T] [LocallyCompactSpace T] [ContinuousConstSMul Γ T] [ProperlyDiscontinuousSMul Γ T] :

T2Space (Quotient (MulAction.orbitRel Γ T))

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

Equations

⋯ = ⋯

theorem ContinuousConstVAdd.secondCountableTopology {Γ : Type u_4} [AddGroup Γ] {T : Type u_5} [TopologicalSpace T] [AddAction Γ T] [SecondCountableTopology T] [ContinuousConstVAdd Γ T] :

SecondCountableTopology (Quotient (AddAction.orbitRel Γ T))

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

theorem ContinuousConstSMul.secondCountableTopology {Γ : Type u_4} [Group Γ] {T : Type u_5} [TopologicalSpace T] [MulAction Γ T] [SecondCountableTopology T] [ContinuousConstSMul Γ T] :

SecondCountableTopology (Quotient (MulAction.orbitRel Γ T))

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 x → c • 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