Documentation

Mathlib.Topology.Algebra.ConstMulAction

Monoid actions continuous in the second variable #

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

Main definitions #

Main results #

Tags #

Hausdorff, discrete group, properly discontinuous, quotient space

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

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

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

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

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

Instances
    theorem ContinuousConstSMul.continuous_const_smul {Γ : Type u_1} {T : Type u_2} :
    ∀ {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.

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

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

      Equations
      • =

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

      Equations
      • =
      Equations
      • =
      Equations
      • =
      Equations
      • = inst
      Equations
      • = inst
      Equations
      • = inst
      Equations
      • = inst
      instance Prod.continuousConstVAdd {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] [TopologicalSpace β] [VAdd M β] [ContinuousConstVAdd M β] :
      Equations
      • =
      instance Prod.continuousConstSMul {M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] [TopologicalSpace β] [SMul M β] [ContinuousConstSMul M β] :
      Equations
      • =
      instance instContinuousConstVAddForall {M : Type u_1} {ι : Type u_4} {γ : ιType u_5} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → VAdd M (γ i)] [∀ (i : ι), ContinuousConstVAdd M (γ i)] :
      ContinuousConstVAdd M ((i : ι) → γ i)
      Equations
      • =
      instance instContinuousConstSMulForall {M : Type u_1} {ι : Type u_4} {γ : ιType u_5} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → SMul M (γ i)] [∀ (i : ι), ContinuousConstSMul M (γ i)] :
      ContinuousConstSMul M ((i : ι) → γ i)
      Equations
      • =
      theorem IsCompact.vadd {α : Type u_4} {β : Type u_5} [VAdd α β] [TopologicalSpace β] [ContinuousConstVAdd α β] (a : α) {s : Set β} (hs : IsCompact s) :
      theorem IsCompact.smul {α : Type u_4} {β : Type u_5} [SMul α β] [TopologicalSpace β] [ContinuousConstSMul α β] (a : α) {s : Set β} (hs : IsCompact s) :
      theorem Specializes.const_vadd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {x : α} {y : α} (h : x y) (c : M) :
      (c +ᵥ x) (c +ᵥ y)
      theorem Specializes.const_smul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {x : α} {y : α} (h : x y) (c : M) :
      (c x) (c y)
      theorem Inseparable.const_vadd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {x : α} {y : α} (h : Inseparable x y) (c : M) :
      Inseparable (c +ᵥ x) (c +ᵥ y)
      theorem Inseparable.const_smul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {x : α} {y : α} (h : Inseparable x y) (c : M) :
      Inseparable (c x) (c y)
      theorem Inducing.continuousConstVAdd {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {N : Type u_4} {β : Type u_5} [VAdd N β] [TopologicalSpace β] {g : βα} (hg : Inducing g) (f : NM) (hf : ∀ {c : N} {x : β}, g (c +ᵥ x) = f c +ᵥ g x) :
      theorem Inducing.continuousConstSMul {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {N : Type u_4} {β : Type u_5} [SMul N β] [TopologicalSpace β] {g : βα} (hg : Inducing g) (f : NM) (hf : ∀ {c : N} {x : β}, g (c x) = f c g x) :
      Equations
      • =
      Equations
      • =
      theorem vadd_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [ContinuousConstVAdd M α] (c : M) (s : Set α) :
      theorem smul_closure_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [ContinuousConstSMul M α] (c : M) (s : Set α) :
      theorem vadd_closure_orbit_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [AddMonoid M] [AddAction M α] [ContinuousConstVAdd M α] (c : M) (x : α) :
      theorem smul_closure_orbit_subset {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [Monoid M] [MulAction M α] [ContinuousConstSMul M α] (c : M) (x : α) :
      theorem isClosed_setOf_map_smul {M : Type u_1} [Monoid M] {N : Type u_4} [Monoid N] (α : Type u_5) (β : Type u_6) [MulAction M α] [MulAction N β] [TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β] (σ : MN) :
      IsClosed {f : αβ | ∀ (c : M) (x : α), f (c x) = σ c f x}
      theorem tendsto_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {f : βα} {l : Filter β} {a : α} (c : G) :
      Filter.Tendsto (fun (x : β) => c +ᵥ f x) l (nhds (c +ᵥ a)) Filter.Tendsto f l (nhds a)
      theorem tendsto_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {f : βα} {l : Filter β} {a : α} (c : G) :
      Filter.Tendsto (fun (x : β) => c f x) l (nhds (c a)) Filter.Tendsto f l (nhds a)
      theorem continuousWithinAt_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] [TopologicalSpace β] {f : βα} {b : β} {s : Set β} (c : G) :
      ContinuousWithinAt (fun (x : β) => c +ᵥ f x) s b ContinuousWithinAt f s b
      theorem continuousWithinAt_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] [TopologicalSpace β] {f : βα} {b : β} {s : Set β} (c : G) :
      ContinuousWithinAt (fun (x : β) => c f x) s b ContinuousWithinAt f s b
      theorem continuousOn_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] [TopologicalSpace β] {f : βα} {s : Set β} (c : G) :
      ContinuousOn (fun (x : β) => c +ᵥ f x) s ContinuousOn f s
      theorem continuousOn_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] [TopologicalSpace β] {f : βα} {s : Set β} (c : G) :
      ContinuousOn (fun (x : β) => c f x) s ContinuousOn f s
      theorem continuousAt_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] [TopologicalSpace β] {f : βα} {b : β} (c : G) :
      ContinuousAt (fun (x : β) => c +ᵥ f x) b ContinuousAt f b
      theorem continuousAt_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] [TopologicalSpace β] {f : βα} {b : β} (c : G) :
      ContinuousAt (fun (x : β) => c f x) b ContinuousAt f b
      theorem continuous_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] [TopologicalSpace β] {f : βα} (c : G) :
      (Continuous fun (x : β) => c +ᵥ f x) Continuous f
      theorem continuous_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] [TopologicalSpace β] {f : βα} (c : G) :
      (Continuous fun (x : β) => c f x) Continuous f
      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
        @[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_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_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_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
        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) :
          theorem IsClosed.smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set α} (hs : IsClosed s) (c : G) :
          theorem closure_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) (s : Set α) :
          theorem closure_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) (s : Set α) :
          closure (c s) = c closure s
          theorem Dense.vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) {s : Set α} (hs : Dense s) :
          Dense (c +ᵥ s)
          theorem Dense.smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) {s : Set α} (hs : Dense s) :
          Dense (c s)
          theorem interior_vadd {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) (s : Set α) :
          theorem interior_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) (s : Set α) :
          theorem IsOpen.vadd_left {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {s : Set G} {t : Set α} (ht : IsOpen t) :
          IsOpen (s +ᵥ t)
          theorem IsOpen.smul_left {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set G} {t : Set α} (ht : IsOpen t) :
          IsOpen (s t)
          theorem subset_interior_vadd_right {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {s : Set G} {t : Set α} :
          theorem subset_interior_smul_right {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {s : Set G} {t : Set α} :
          @[simp]
          theorem vadd_mem_nhds_vadd_iff {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {t : Set α} (g : G) {a : α} :
          g +ᵥ t nhds (g +ᵥ a) t nhds a
          @[simp]
          theorem smul_mem_nhds_smul_iff {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {t : Set α} (g : G) {a : α} :
          g t nhds (g a) t nhds a
          theorem smul_mem_nhds_smul {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {t : Set α} (g : G) {a : α} :
          t nhds ag t nhds (g a)

          Alias of the reverse direction of smul_mem_nhds_smul_iff.

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

          Alias of the reverse direction of smul_mem_nhds_smul_iff.


          Alias of the reverse direction of smul_mem_nhds_smul_iff.

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

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

          Equations
          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 α) :
            theorem closure_smul₀' {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} (hc : c 0) (s : Set α) :
            closure (c s) = c closure s
            theorem closure_smul₀ {G₀ : Type u_4} [GroupWithZero G₀] {E : Type u_5} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) (s : Set E) :
            closure (c s) = c closure s
            theorem isClosedMap_smul_of_ne_zero {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {c : G₀} (hc : c 0) :
            IsClosedMap fun (x : α) => c x

            smul is a closed map in the second argument.

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

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

            smul is a closed map in the second argument.

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

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

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

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

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

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

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

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

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

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

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

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

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

                @[instance 100]

                A finite group action is always properly discontinuous.

                Equations
                • =
                @[instance 100]

                A finite group action is always properly discontinuous.

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

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

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

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

                @[instance 100]

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

                Equations
                • =
                @[instance 100]

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

                Equations
                • =

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

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

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

                Scalar multiplication by a nonzero scalar preserves neighborhoods.

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

                Alias of smul_mem_nhds_smul_iff₀.


                Scalar multiplication by a nonzero scalar preserves neighborhoods.

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

                Alias of the reverse direction of smul_mem_nhds_smul_iff₀.


                Scalar multiplication by a nonzero scalar preserves neighborhoods.

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