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 mapx ↦ γ • xis continuous onT;ProperlyDiscontinuousSMul: says that the scalar multiplication(•) : Γ → T → Tis properly discontinuous, that is, for any pair of compact setsK, LinT, only finitely manyγ:ΓmoveKto have nontrivial intersection withL.Homeomorph.smul: scalar multiplication by an element of a groupΓacting onTis a homeomorphism ofT.
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
- continuous_const_smul : ∀ (γ : Γ), Continuous fun x => γ • x
The scalar multiplication
(•) : Γ → T → Tis continuous in the second argument.
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 α.
Instances
- continuous_const_vadd : ∀ (γ : Γ), Continuous fun x => γ +ᵥ x
The additive action
(+ᵥ) : Γ → T → Tis continuous in the second argument.
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 α.
Instances
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
theorem
ContinuousConstVAdd.op.proof_1
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[VAdd M α]
[ContinuousConstVAdd M α]
[VAdd Mᵃᵒᵖ α]
[IsCentralVAdd M α]
:
instance
ContinuousConstVAdd.op
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[VAdd M α]
[ContinuousConstVAdd M α]
[VAdd Mᵃᵒᵖ α]
[IsCentralVAdd M α]
:
If an additive action is central, then its right action is continuous when its left action is.
instance
ContinuousConstSMul.op
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[SMul M α]
[ContinuousConstSMul M α]
[SMul Mᵐᵒᵖ α]
[IsCentralScalar M α]
:
If a scalar is central, then its right action is continuous when its left action is.
theorem
AddOpposite.continuousConstVAdd.proof_1
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[VAdd M α]
[ContinuousConstVAdd M α]
:
instance
AddOpposite.continuousConstVAdd
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[VAdd M α]
[ContinuousConstVAdd M α]
:
instance
MulOpposite.continuousConstSMul
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[SMul M α]
[ContinuousConstSMul M α]
:
instance
instContinuousConstVAddOrderDualInstTopologicalSpaceOrderDualInstVAdd
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[VAdd M α]
[ContinuousConstVAdd M α]
:
Equations
- (_ : ContinuousConstVAdd M αᵒᵈ) = inst
instance
instContinuousConstSMulOrderDualInstTopologicalSpaceOrderDualInstSMul
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[SMul M α]
[ContinuousConstSMul M α]
:
Equations
- (_ : ContinuousConstSMul M αᵒᵈ) = inst
instance
OrderDual.continuousConstVAdd'
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[VAdd M α]
[ContinuousConstVAdd M α]
:
Equations
- (_ : ContinuousConstVAdd Mᵒᵈ α) = inst
instance
OrderDual.continuousConstSMul'
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[SMul M α]
[ContinuousConstSMul M α]
:
Equations
- (_ : ContinuousConstSMul Mᵒᵈ α) = 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 (α × β)
theorem
Prod.continuousConstVAdd.proof_1
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[TopologicalSpace α]
[VAdd M α]
[ContinuousConstVAdd M α]
[TopologicalSpace β]
[VAdd M β]
[ContinuousConstVAdd M β]
:
ContinuousConstVAdd M (α × β)
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 (α × β)
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)
theorem
instContinuousConstVAddForAllTopologicalSpaceInstVAdd.proof_1
{M : Type u_1}
{ι : Type u_2}
{γ : ι → Type u_3}
[(i : ι) → TopologicalSpace (γ i)]
[(i : ι) → VAdd M (γ i)]
[∀ (i : ι), ContinuousConstVAdd M (γ i)]
:
ContinuousConstVAdd M ((i : ι) → γ i)
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)
theorem
IsCompact.vadd
{α : Type u_4}
{β : Type u_5}
[VAdd α β]
[TopologicalSpace β]
[ContinuousConstVAdd α β]
(a : α)
{s : Set β}
(hs : IsCompact s)
:
theorem
IsCompact.smul
{α : Type u_4}
{β : Type u_5}
[SMul α β]
[TopologicalSpace β]
[ContinuousConstSMul α β]
(a : α)
{s : Set β}
(hs : IsCompact s)
:
instance
AddUnits.continuousConstVAdd
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[AddMonoid M]
[AddAction M α]
[ContinuousConstVAdd M α]
:
ContinuousConstVAdd (AddUnits M) α
theorem
AddUnits.continuousConstVAdd.proof_1
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[AddMonoid M]
[AddAction M α]
[ContinuousConstVAdd M α]
:
ContinuousConstVAdd (AddUnits M) α
instance
Units.continuousConstSMul
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[Monoid M]
[MulAction M α]
[ContinuousConstSMul M α]
:
theorem
vadd_closure_subset
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[AddMonoid M]
[AddAction M α]
[ContinuousConstVAdd M α]
(c : M)
(s : Set α)
:
theorem
smul_closure_subset
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[Monoid M]
[MulAction M α]
[ContinuousConstSMul M α]
(c : M)
(s : Set α)
:
theorem
vadd_closure_orbit_subset
{M : Type u_1}
{α : Type u_2}
[TopologicalSpace α]
[AddMonoid M]
[AddAction M α]
[ContinuousConstVAdd M α]
(c : M)
(x : α)
:
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
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
Instances For
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
Instances For
theorem
isOpenMap_vadd
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[AddGroup G]
[AddAction G α]
[ContinuousConstVAdd G α]
(c : G)
:
theorem
isOpenMap_smul
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[Group G]
[MulAction G α]
[ContinuousConstSMul G α]
(c : G)
:
theorem
IsOpen.vadd
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[AddGroup G]
[AddAction G α]
[ContinuousConstVAdd G α]
{s : Set α}
(hs : IsOpen s)
(c : G)
:
theorem
IsOpen.smul
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[Group G]
[MulAction G α]
[ContinuousConstSMul G α]
{s : Set α}
(hs : IsOpen s)
(c : G)
:
theorem
isClosedMap_vadd
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[AddGroup G]
[AddAction G α]
[ContinuousConstVAdd G α]
(c : G)
:
IsClosedMap fun x => c +ᵥ x
theorem
isClosedMap_smul
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[Group G]
[MulAction G α]
[ContinuousConstSMul G α]
(c : G)
:
IsClosedMap fun x => c • x
theorem
IsClosed.vadd
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[AddGroup G]
[AddAction G α]
[ContinuousConstVAdd G α]
{s : Set α}
(hs : IsClosed s)
(c : G)
:
theorem
IsClosed.smul
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[Group G]
[MulAction G α]
[ContinuousConstSMul G α]
{s : Set α}
(hs : IsClosed s)
(c : G)
:
theorem
closure_vadd
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[AddGroup G]
[AddAction G α]
[ContinuousConstVAdd G α]
(c : G)
(s : Set α)
:
theorem
closure_smul
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[Group G]
[MulAction G α]
[ContinuousConstSMul G α]
(c : G)
(s : Set α)
:
theorem
Dense.vadd
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[AddGroup G]
[AddAction G α]
[ContinuousConstVAdd G α]
(c : G)
{s : Set α}
(hs : Dense 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)
:
theorem
interior_vadd
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[AddGroup G]
[AddAction G α]
[ContinuousConstVAdd G α]
(c : G)
(s : Set α)
:
theorem
interior_smul
{α : Type u_2}
{G : Type u_4}
[TopologicalSpace α]
[Group G]
[MulAction G α]
[ContinuousConstSMul G α]
(c : G)
(s : Set α)
:
theorem
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.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)
:
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)
:
theorem
interior_smul₀
{α : Type u_2}
{G₀ : Type u_4}
[TopologicalSpace α]
[GroupWithZero G₀]
[MulAction G₀ α]
[ContinuousConstSMul G₀ α]
{c : G₀}
(hc : c ≠ 0)
(s : Set α)
:
theorem
closure_smul₀
{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)
:
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)
:
theorem
isClosedMap_smul₀
{𝕜 : Type u_5}
{M : Type u_6}
[DivisionRing 𝕜]
[AddCommMonoid M]
[TopologicalSpace M]
[T1Space M]
[Module 𝕜 M]
[ContinuousConstSMul 𝕜 M]
(c : 𝕜)
:
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₀
{𝕜 : Type u_5}
{M : Type u_6}
[DivisionRing 𝕜]
[AddCommMonoid M]
[TopologicalSpace M]
[T1Space M]
[Module 𝕜 M]
[ContinuousConstSMul 𝕜 M]
(c : 𝕜)
{s : Set M}
(hs : IsClosed s)
:
theorem
HasCompactMulSupport.comp_smul
{α : Type u_2}
{G₀ : Type u_4}
[TopologicalSpace α]
[GroupWithZero G₀]
[MulAction G₀ α]
[ContinuousConstSMul G₀ α]
{β : Type u_5}
[One β]
{f : α → β}
(h : HasCompactMulSupport f)
{c : G₀}
(hc : c ≠ 0)
:
HasCompactMulSupport fun x => f (c • x)
theorem
HasCompactSupport.comp_smul
{α : Type u_2}
{G₀ : Type u_4}
[TopologicalSpace α]
[GroupWithZero G₀]
[MulAction G₀ α]
[ContinuousConstSMul G₀ α]
{β : Type u_5}
[Zero β]
{f : α → β}
(h : HasCompactSupport f)
{c : G₀}
(hc : c ≠ 0)
:
HasCompactSupport fun x => f (c • x)
theorem
IsUnit.tendsto_const_smul_iff
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Monoid M]
[TopologicalSpace α]
[MulAction M α]
[ContinuousConstSMul M α]
{f : β → α}
{l : Filter β}
{a : α}
{c : M}
(hc : IsUnit c)
:
Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a)
theorem
IsUnit.continuousWithinAt_const_smul_iff
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Monoid M]
[TopologicalSpace α]
[MulAction M α]
[ContinuousConstSMul M α]
[TopologicalSpace β]
{f : β → α}
{b : β}
{c : M}
{s : Set β}
(hc : IsUnit c)
:
ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b
theorem
IsUnit.continuousOn_const_smul_iff
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Monoid M]
[TopologicalSpace α]
[MulAction M α]
[ContinuousConstSMul M α]
[TopologicalSpace β]
{f : β → α}
{c : M}
{s : Set β}
(hc : IsUnit c)
:
ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s
theorem
IsUnit.continuousAt_const_smul_iff
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Monoid M]
[TopologicalSpace α]
[MulAction M α]
[ContinuousConstSMul M α]
[TopologicalSpace β]
{f : β → α}
{b : β}
{c : M}
(hc : IsUnit c)
:
ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b
theorem
IsUnit.continuous_const_smul_iff
{M : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Monoid M]
[TopologicalSpace α]
[MulAction M α]
[ContinuousConstSMul M α]
[TopologicalSpace β]
{f : β → α}
{c : M}
(hc : IsUnit c)
:
(Continuous fun x => c • f x) ↔ Continuous f
theorem
IsUnit.isOpenMap_smul
{M : Type u_1}
{α : Type u_2}
[Monoid M]
[TopologicalSpace α]
[MulAction M α]
[ContinuousConstSMul M α]
{c : M}
(hc : IsUnit c)
:
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
- finite_disjoint_inter_image : ∀ {K L : Set T}, IsCompact K → IsCompact L → Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
Given two compact sets
KandL,γ • K ∩ Lis nonempty for finitely manyγ.
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.
Instances
- finite_disjoint_inter_image : ∀ {K L : Set T}, IsCompact K → IsCompact L → Set.Finite {γ | (fun x => γ +ᵥ x) '' K ∩ L ≠ ∅}
Given two compact sets
KandL,γ +ᵥ K ∩ Lis nonempty for finitely manyγ.
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.
Instances
instance
Finite.to_properlyDiscontinuousVAdd
{Γ : Type u_4}
[AddGroup Γ]
{T : Type u_5}
[TopologicalSpace T]
[AddAction Γ T]
[Finite Γ]
:
A finite group action is always properly discontinuous.
theorem
Finite.to_properlyDiscontinuousVAdd.proof_1
{Γ : Type u_1}
[AddGroup Γ]
{T : Type u_2}
[TopologicalSpace T]
[AddAction Γ T]
[Finite Γ]
:
instance
Finite.to_properlyDiscontinuousSMul
{Γ : Type u_4}
[Group Γ]
{T : Type u_5}
[TopologicalSpace T]
[MulAction Γ T]
[Finite Γ]
:
A finite group action is always properly discontinuous.
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.
theorem
t2Space_of_properlyDiscontinuousVAdd_of_t2Space.proof_1
{Γ : Type u_1}
[AddGroup Γ]
{T : Type u_2}
[TopologicalSpace T]
[AddAction Γ T]
[T2Space T]
[LocallyCompactSpace T]
[ContinuousConstVAdd Γ T]
[ProperlyDiscontinuousVAdd Γ T]
:
T2Space (Quotient (AddAction.orbitRel Γ T))
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.
theorem
ContinuousConstVAdd.secondCountableTopology
{Γ : Type u_4}
[AddGroup Γ]
{T : Type u_5}
[TopologicalSpace T]
[AddAction Γ T]
[TopologicalSpace.SecondCountableTopology T]
[ContinuousConstVAdd Γ 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]
[TopologicalSpace.SecondCountableTopology T]
[ContinuousConstSMul Γ 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)
:
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)
:
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)
: