# 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`. *`Homeomorph.smulOfNeZero`: if a group with zero `G₀` (e.g., a field) acts on `X` and `c : G₀` is a nonzero element of `G₀`, then scalar multiplication by `c` is a homeomorphism of `X`;
- `Homeomorph.smul`: scalar multiplication by an element of a group `G` acting on `X` is a homeomorphism of `X`.

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

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

Instances

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

Instances

source
instance instContinuousConstSMulULift {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] :
ContinuousConstSMul (ULift.{u_4, u_1} M) α
source
instance instContinuousConstVAddULift {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] :
ContinuousConstVAdd (ULift.{u_4, u_1} M) α
source
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 : Tendsto f l (nhds a)) (c : M) :
Tendsto (fun (x : β) => c • f x) l (nhds (c • a))
source
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 : Tendsto f l (nhds a)) (c : M) :
Tendsto (fun (x : β) => c +ᵥ f x) l (nhds (c +ᵥ a))
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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.

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

source
instance MulOpposite.continuousConstSMul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] :
ContinuousConstSMul M α ᵐᵒᵖ
source
instance AddOpposite.continuousConstVAdd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] :
ContinuousConstVAdd M α ᵃᵒᵖ
source
instance instContinuousConstSMulOrderDual {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] :
ContinuousConstSMul M α ᵒᵈ
source
instance instContinuousConstVAddOrderDual {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] :
ContinuousConstVAdd M α ᵒᵈ
source
instance OrderDual.continuousConstSMul' {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] :
ContinuousConstSMul M ᵒᵈ α
source
instance OrderDual.continuousConstVAdd' {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] :
ContinuousConstVAdd M ᵒᵈ α
source
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 (α × β)
source
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 (α × β)
source
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)
source
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)
source
theorem IsCompact.smul {α : Type u_4} {β : Type u_5} [SMul α β] [TopologicalSpace β] [ContinuousConstSMul α β] (a : α) {s : Set β} (hs : IsCompact s) :
IsCompact (a • s)
source
theorem IsCompact.vadd {α : Type u_4} {β : Type u_5} [VAdd α β] [TopologicalSpace β] [ContinuousConstVAdd α β] (a : α) {s : Set β} (hs : IsCompact s) :
IsCompact (a +ᵥ s)
source
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)
source
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)
source
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)
source
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)
source
theorem Topology.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 β
source
theorem Topology.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 β
source
theorem smul_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] (c : M) (s : Set α) :
c • closure s ⊆ closure (c • s)
source
theorem vadd_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] (c : M) (s : Set α) :
c +ᵥ closure s ⊆ closure (c +ᵥ s)
source
theorem set_smul_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] (s : Set M) (t : Set α) :
s • closure t ⊆ closure (s • t)
source
theorem set_vadd_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] (s : Set M) (t : Set α) :
s +ᵥ closure t ⊆ closure (s +ᵥ t)
source
theorem isClosed_setOf_map_smul {M : Type u_1} {N : Type u_4} (α : Type u_5) (β : Type u_6) [SMul M α] [SMul N β] [TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β] (σ : M → N) :
IsClosed {f : α → β | ∀ (c : M) (x : α), f (c • x) = σ c • f x}
source
instance Units.continuousConstSMul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [ContinuousConstSMul M α] :
ContinuousConstSMul M ˣ α
source
instance AddUnits.continuousConstVAdd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [ContinuousConstVAdd M α] :
ContinuousConstVAdd (AddUnits M) α
source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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

source
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

source
@[simp]
theorem Homeomorph.smul_apply {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (γ : G) (x : α) :
(smul γ) x = γ • x
source
@[simp]
theorem Homeomorph.smul_symm_apply {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (γ : G) (x : α) :
(smul γ).symm x = γ⁻¹ • x
source
@[simp]
theorem Homeomorph.vadd_apply {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (γ : G) (x : α) :
(vadd γ) x = γ +ᵥ x
source
@[simp]
theorem Homeomorph.vadd_symm_apply {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (γ : G) (x : α) :
(vadd γ).symm x = -γ +ᵥ x
source
theorem isOpenMap_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) :
IsOpenMap fun (x : α) => c • x
source
theorem isOpenMap_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) :
IsOpenMap fun (x : α) => c +ᵥ x
source
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)
source
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)
source
theorem isClosedMap_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) :
IsClosedMap fun (x : α) => c • x
source
theorem isClosedMap_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) :
IsClosedMap fun (x : α) => c +ᵥ x
source
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)
source
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)
source
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
source
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
source
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)
source
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)
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
@[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
source
@[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
source
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`.

source
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)
source
@[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
source
@[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
source
theorem MulAction.IsPretransitive.t1Space_iff {α : Type u_2} (G : Type u_4) [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (x : α) [IsPretransitive G α] :
T1Space α ↔ IsClosed {x}
source
theorem AddAction.IsPretransitive.t1Space_iff {α : Type u_2} (G : Type u_4) [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (x : α) [IsPretransitive G α] :
T1Space α ↔ IsClosed {x}
source
theorem MulAction.IsPretransitive.discreteTopology_iff {α : Type u_2} (G : Type u_4) [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (x : α) [IsPretransitive G α] :
DiscreteTopology α ↔ IsOpen {x}
source
theorem AddAction.IsPretransitive.discreteTopology_iff {α : Type u_2} (G : Type u_4) [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (x : α) [IsPretransitive G α] :
DiscreteTopology α ↔ IsOpen {x}
source
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)
source
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
source
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
source
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
source
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
source
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

source
@[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
source
@[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
source
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
source
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)
source
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
source
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
source
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
source
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`.

source
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)
source
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`.

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

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

Instances

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

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

Instances

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

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

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

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

source
theorem MulAction.isOpenQuotientMap_quotientMk {Γ : Type u_4} [Group Γ] {T : Type u_5} [TopologicalSpace T] [MulAction Γ T] [ContinuousConstSMul Γ T] :
IsOpenQuotientMap (Quotient.mk (orbitRel Γ T))
source
theorem AddAction.isOpenQuotientMap_quotientMk {Γ : Type u_4} [AddGroup Γ] {T : Type u_5} [TopologicalSpace T] [AddAction Γ T] [ContinuousConstVAdd Γ T] :
IsOpenQuotientMap (Quotient.mk (orbitRel Γ T))
source
@[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.

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

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

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

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

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

source
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