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

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.

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

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

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

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 instContinuousConstVAddOrderDualInstTopologicalSpaceOrderDualInstVAdd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] : ContinuousConstVAdd M αᵒᵈ

Equations

• ⋯ = inst

instance instContinuousConstSMulOrderDualInstTopologicalSpaceOrderDualInstSMul {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 instContinuousConstVAddForAllTopologicalSpaceInstVAdd {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 instContinuousConstSMulForAllTopologicalSpaceInstSMul {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)

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_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 := ⋯ }

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.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 := ⋯ }

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

@[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.symm (Homeomorph.smulOfNeZero c hc)) = 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.NormedSpace.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.NormedSpace.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

class ProperlyDiscontinuousSMul (Γ : Type u_4) (T : Type u_5) [TopologicalSpace T] [SMul Γ T] : Prop

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 → Set.Finite {γ : Γ | (fun (x : T) => γ • x) '' K ∩ L ≠ ∅}

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

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 → Set.Finite {γ : Γ | (fun (x : T) => γ +ᵥ x) '' K ∩ L ≠ ∅}

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

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

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

Scalar multiplication preserves neighborhoods.

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

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