Mathlib.Topology.Algebra.MulAction

ContinuousSMul structure

(M X : Type*) [SMul M X] [TopologicalSpace M] [TopologicalSpace X]

Full source

/-- Class `ContinuousSMul M X` says that the scalar multiplication `(•) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
including (semi)modules and algebras. -/
class ContinuousSMul (M X : Type*) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] :
    Prop where
  /-- The scalar multiplication `(•)` is continuous. -/
  continuous_smul : Continuous fun p : M × X => p.1 • p.2

Continuous Scalar Multiplication

Informal description

The structure `ContinuousSMul M X` represents the property that the scalar multiplication operation `(•) : M × X → X` is jointly continuous in both arguments, where `M` is a type with a scalar multiplication action on `X`, and both `M` and `X` are equipped with topological spaces. This class is used for various multiplicative actions, including (semi)modules and algebras.

ContinuousVAdd structure

(M X : Type*) [VAdd M X] [TopologicalSpace M] [TopologicalSpace X]

Full source

/-- Class `ContinuousVAdd M X` says that the additive action `(+ᵥ) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of additive actions,
including (semi)modules and algebras. -/
class ContinuousVAdd (M X : Type*) [VAdd M X] [TopologicalSpace M] [TopologicalSpace X] :
    Prop where
  /-- The additive action `(+ᵥ)` is continuous. -/
  continuous_vadd : Continuous fun p : M × X => p.1 +ᵥ p.2

Continuous Additive Action

Informal description

The structure `ContinuousVAdd M X` asserts that the additive action `(+ᵥ) : M → X → X` is continuous in both arguments, where `M` and `X` are topological spaces. This class is used for various types of additive actions, including (semi)modules and algebras.

IsScalarTower.continuousSMul theorem

 {M : Type*} (N : Type*) {α : Type*} [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α]
  [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace α] [ContinuousSMul M N] [ContinuousSMul N α] :
  ContinuousSMul M α

Full source

lemma IsScalarTower.continuousSMul {M : Type*} (N : Type*) {α : Type*} [Monoid N] [SMul M N]
    [MulAction N α] [SMul M α] [IsScalarTower M N α] [TopologicalSpace M] [TopologicalSpace N]
    [TopologicalSpace α] [ContinuousSMul M N] [ContinuousSMul N α] : ContinuousSMul M α :=
  { continuous_smul := by
      suffices Continuous (fun p : M × α ↦ (p.1 • (1 : N)) • p.2) by simpa
      fun_prop }

Continuity of Scalar Multiplication in a Scalar Tower

Informal description

Let $M$, $N$, and $\alpha$ be types with the following structures: - $N$ is a monoid with a scalar multiplication action $M \times N \to N$ and a multiplicative action $N \times \alpha \to \alpha$, - There is a scalar multiplication action $M \times \alpha \to \alpha$ forming a scalar tower, i.e., $(m \cdot n) \cdot x = m \cdot (n \cdot x)$ for all $m \in M$, $n \in N$, $x \in \alpha$, - $M$, $N$, and $\alpha$ are equipped with topological spaces, - The scalar multiplications $M \times N \to N$ and $N \times \alpha \to \alpha$ are continuous. Then the scalar multiplication $M \times \alpha \to \alpha$ is also continuous.

instContinuousSMulULift instance

: ContinuousSMul (ULift M) X

Full source

@[to_additive]
instance : ContinuousSMul (ULift M) X :=
  ⟨(continuous_smul (M := M)).comp₂ (continuous_uliftDown.comp continuous_fst) continuous_snd⟩

Continuous Scalar Multiplication on Universe-Lifted Types

Informal description

For any type $M$ with a scalar multiplication action on $X$ and topological spaces on $M$ and $X$, the scalar multiplication operation $(•) : \text{ULift}\, M × X → X$ is jointly continuous, where $\text{ULift}\, M$ is the universe-lifted version of $M$.

ContinuousSMul.continuousConstSMul instance

: ContinuousConstSMul M X

Full source

@[to_additive]
instance (priority := 100) ContinuousSMul.continuousConstSMul : ContinuousConstSMul M X where
  continuous_const_smul _ := continuous_smul.comp (continuous_const.prodMk continuous_id)

Continuous Scalar Multiplication Implies Continuous Constant Multiplication

Informal description

For any types $M$ and $X$ with a scalar multiplication action $M \times X \to X$ and topological spaces on $M$ and $X$, if the scalar multiplication is jointly continuous (i.e., $M$ acts continuously on $X$), then for each fixed $m \in M$, the map $x \mapsto m \bullet x$ is continuous.

ContinuousSMul.induced theorem

 {R : Type*} {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Semiring R] [AddCommMonoid α] [AddCommMonoid β]
  [Module R α] [Module R β] [TopologicalSpace R] [LinearMapClass F R α β] [tβ : TopologicalSpace β] [ContinuousSMul R β]
  (f : F) : @ContinuousSMul R α _ _ (tβ.induced f)

Full source

theorem ContinuousSMul.induced {R : Type*} {α : Type*} {β : Type*} {F : Type*} [FunLike F α β]
    [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β]
    [TopologicalSpace R] [LinearMapClass F R α β] [tβ : TopologicalSpace β] [ContinuousSMul R β]
    (f : F) : @ContinuousSMul R α _ _ (tβ.induced f) := by
  let tα := tβ.induced f
  refine ⟨continuous_induced_rng.2 ?_⟩
  simp only [Function.comp_def, map_smul]
  fun_prop

Continuity of Induced Scalar Multiplication under Linear Maps

Informal description

Let $R$ be a semiring, and let $\alpha$ and $\beta$ be additive commutative monoids equipped with $R$-module structures. Suppose $\beta$ has a topological space structure and $R$ acts continuously on $\beta$ via scalar multiplication. Given a linear map $f \colon \alpha \to \beta$ (where $F$ is a type of linear maps), the induced topology on $\alpha$ (defined as the coarsest topology making $f$ continuous) ensures that the scalar multiplication $R \times \alpha \to \alpha$ is also continuous.

Filter.Tendsto.smul theorem

 {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X} (hf : Tendsto f l (𝓝 c)) (hg : Tendsto g l (𝓝 a)) :
  Tendsto (fun x => f x • g x) l (𝓝 <| c • a)

Full source

@[to_additive]
theorem Filter.Tendsto.smul {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X}
    (hf : Tendsto f l (𝓝 c)) (hg : Tendsto g l (𝓝 a)) :
    Tendsto (fun x => f x • g x) l (𝓝 <| c • a) :=
  (continuous_smul.tendsto _).comp (hf.prodMk_nhds hg)

Limit of Scalar Multiplication of Convergent Functions

Informal description

Let $f \colon \alpha \to M$ and $g \colon \alpha \to X$ be functions, and let $l$ be a filter on $\alpha$. If $f$ tends to $c \in M$ along $l$ and $g$ tends to $a \in X$ along $l$, then the function $x \mapsto f(x) \bullet g(x)$ tends to $c \bullet a$ along $l$.

Filter.Tendsto.smul_const theorem

 {f : α → M} {l : Filter α} {c : M} (hf : Tendsto f l (𝓝 c)) (a : X) : Tendsto (fun x => f x • a) l (𝓝 (c • a))

Full source

@[to_additive]
theorem Filter.Tendsto.smul_const {f : α → M} {l : Filter α} {c : M} (hf : Tendsto f l (𝓝 c))
    (a : X) : Tendsto (fun x => f x • a) l (𝓝 (c • a)) :=
  hf.smul tendsto_const_nhds

Limit of Scalar Multiplication with Constant Vector

Informal description

Let $f \colon \alpha \to M$ be a function and $l$ be a filter on $\alpha$. If $f$ tends to $c \in M$ along $l$, then for any fixed element $a \in X$, the function $x \mapsto f(x) \bullet a$ tends to $c \bullet a$ along $l$.

ContinuousWithinAt.smul theorem

(hf : ContinuousWithinAt f s b) (hg : ContinuousWithinAt g s b) : ContinuousWithinAt (fun x => f x • g x) s b

Full source

@[to_additive]
theorem ContinuousWithinAt.smul (hf : ContinuousWithinAt f s b) (hg : ContinuousWithinAt g s b) :
    ContinuousWithinAt (fun x => f x • g x) s b :=
  Filter.Tendsto.smul hf hg

Continuity of Scalar Multiplication Within a Subset at a Point

Informal description

Let $f$ and $g$ be functions defined on a topological space, and let $s$ be a subset of the domain. If $f$ is continuous within $s$ at a point $b$ and $g$ is continuous within $s$ at $b$, then the function $x \mapsto f(x) \bullet g(x)$ is continuous within $s$ at $b$, where $\bullet$ denotes the scalar multiplication operation.

ContinuousAt.smul theorem

(hf : ContinuousAt f b) (hg : ContinuousAt g b) : ContinuousAt (fun x => f x • g x) b

Full source

@[to_additive (attr := fun_prop)]
theorem ContinuousAt.smul (hf : ContinuousAt f b) (hg : ContinuousAt g b) :
    ContinuousAt (fun x => f x • g x) b :=
  Filter.Tendsto.smul hf hg

Continuity of Scalar Multiplication at a Point

Informal description

Let $f$ and $g$ be functions such that $f$ is continuous at $b$ and $g$ is continuous at $b$. Then the function $x \mapsto f(x) \bullet g(x)$ is continuous at $b$, where $\bullet$ denotes the scalar multiplication operation.

ContinuousOn.smul theorem

(hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun x => f x • g x) s

Full source

@[to_additive (attr := fun_prop)]
theorem ContinuousOn.smul (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun x => f x • g x) s := fun x hx => (hf x hx).smul (hg x hx)

Continuity of Scalar Multiplication on a Subset

Informal description

Let $f$ and $g$ be functions defined on a topological space, and let $s$ be a subset of the domain. If $f$ is continuous on $s$ and $g$ is continuous on $s$, then the function $x \mapsto f(x) \bullet g(x)$ is continuous on $s$, where $\bullet$ denotes the scalar multiplication operation.

Continuous.smul theorem

(hf : Continuous f) (hg : Continuous g) : Continuous fun x => f x • g x

Full source

@[to_additive (attr := continuity, fun_prop)]
theorem Continuous.smul (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f x • g x :=
  continuous_smul.comp (hf.prodMk hg)

Continuity of Pointwise Scalar Multiplication

Informal description

Let $f$ and $g$ be continuous functions. Then the function $x \mapsto f(x) \cdot g(x)$ is continuous, where $\cdot$ denotes the scalar multiplication operation.

ContinuousSMul.op instance

[SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : ContinuousSMul Mᵐᵒᵖ X

Full source

/-- If a scalar action is central, then its right action is continuous when its left action is. -/
@[to_additive "If an additive action is central, then its right action is continuous when its left
action is."]
instance ContinuousSMul.op [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : ContinuousSMul Mᵐᵒᵖ X :=
  ⟨by
    suffices Continuous fun p : M × X => MulOpposite.op p.fst • p.snd from
      this.comp (MulOpposite.continuous_unop.prodMap continuous_id)
    simpa only [op_smul_eq_smul] using (continuous_smul : Continuous fun p : M × X => _)⟩

Continuity of Right Scalar Multiplication from Central Actions

Informal description

For any type $M$ with a scalar multiplication action on $X$ where the action is central (i.e., the left and right actions coincide), if the left scalar multiplication is continuous, then the right scalar multiplication is also continuous.

MulOpposite.continuousSMul instance

: ContinuousSMul M Xᵐᵒᵖ

Full source

@[to_additive]
instance MulOpposite.continuousSMul : ContinuousSMul M Xᵐᵒᵖ :=
  ⟨MulOpposite.continuous_op.comp <|
      continuous_smul.comp <| continuous_id.prodMap MulOpposite.continuous_unop⟩

Continuous Scalar Multiplication on Opposite Spaces

Informal description

For any topological space $M$ acting continuously on a topological space $X$ via scalar multiplication, the opposite space $X^\text{op}$ also has a continuous scalar multiplication structure induced by $M$.

Specializes.smul theorem

{a b : M} {x y : X} (h₁ : a ⤳ b) (h₂ : x ⤳ y) : (a • x) ⤳ (b • y)

Full source

@[to_additive]
protected theorem Specializes.smul {a b : M} {x y : X} (h₁ : a ⤳ b) (h₂ : x ⤳ y) :
    (a • x) ⤳ (b • y) :=
  (h₁.prod h₂).map continuous_smul

Specialization is preserved under continuous scalar multiplication

Informal description

Let $M$ be a topological space acting continuously on another topological space $X$ via scalar multiplication. For any elements $a, b \in M$ and $x, y \in X$, if $a$ specializes to $b$ and $x$ specializes to $y$, then the scalar product $a \cdot x$ specializes to $b \cdot y$.

Inseparable.smul theorem

{a b : M} {x y : X} (h₁ : Inseparable a b) (h₂ : Inseparable x y) : Inseparable (a • x) (b • y)

Full source

@[to_additive]
protected theorem Inseparable.smul {a b : M} {x y : X} (h₁ : Inseparable a b)
    (h₂ : Inseparable x y) : Inseparable (a • x) (b • y) :=
  (h₁.prod h₂).map continuous_smul

Inseparability is preserved under continuous scalar multiplication

Informal description

Let $M$ be a topological space acting continuously on another topological space $X$ via scalar multiplication. For any elements $a, b \in M$ and $x, y \in X$, if $a$ is inseparable from $b$ and $x$ is inseparable from $y$, then the scalar product $a \cdot x$ is inseparable from $b \cdot y$.

IsCompact.smul_set theorem

{k : Set M} {u : Set X} (hk : IsCompact k) (hu : IsCompact u) : IsCompact (k • u)

Full source

@[to_additive]
lemma IsCompact.smul_set {k : Set M} {u : Set X} (hk : IsCompact k) (hu : IsCompact u) :
    IsCompact (k • u) := by
  rw [← Set.image_smul_prod]
  exact IsCompact.image (hk.prod hu) continuous_smul

Compactness of Scalar Multiplication on Compact Sets

Informal description

For any compact subsets $K \subseteq M$ and $L \subseteq X$ in a topological space with continuous scalar multiplication, the set $\{k \cdot x \mid k \in K, x \in L\}$ is compact.

smul_set_closure_subset theorem

(K : Set M) (L : Set X) : closure K • closure L ⊆ closure (K • L)

Full source

@[to_additive]
lemma smul_set_closure_subset (K : Set M) (L : Set X) :
    closureclosure K • closure L ⊆ closure (K • L) :=
  Set.smul_subset_iff.2 fun _x hx _y hy ↦ map_mem_closure₂ continuous_smul hx hy fun _a ha _b hb ↦
    Set.smul_mem_smul ha hb

Closure of Scalar Multiplication is Contained in Scalar Multiplication of Closures

Informal description

For any subsets $K \subseteq M$ and $L \subseteq X$ in a topological space with continuous scalar multiplication, the scalar multiplication of the closures of $K$ and $L$ is contained in the closure of the scalar multiplication of $K$ and $L$, i.e., $\overline{K} \cdot \overline{L} \subseteq \overline{K \cdot L}$.

Topology.IsInducing.continuousSMul theorem

 {N : Type*} [SMul N Y] [TopologicalSpace N] {f : N → M} (hg : IsInducing g) (hf : Continuous f)
  (hsmul : ∀ {c x}, g (c • x) = f c • g x) : ContinuousSMul N Y

Full source

/-- Suppose that `N` acts on `X` and `M` continuously acts on `Y`.
Suppose that `g : Y → X` is an action homomorphism in the following sense:
there exists a continuous function `f : N → M` such that `g (c • x) = f c • g x`.
Then the action of `N` on `X` is continuous as well.

In many cases, `f = id` so that `g` is an action homomorphism in the sense of `MulActionHom`.
However, this version also works for semilinear maps and `f = Units.val`. -/
@[to_additive
  "Suppose that `N` additively acts on `X` and `M` continuously additively acts on `Y`.
Suppose that `g : Y → X` is an additive action homomorphism in the following sense:
there exists a continuous function `f : N → M` such that `g (c +ᵥ x) = f c +ᵥ g x`.
Then the action of `N` on `X` is continuous as well.

In many cases, `f = id` so that `g` is an action homomorphism in the sense of `AddActionHom`.
However, this version also works for `f = AddUnits.val`."]
lemma Topology.IsInducing.continuousSMul {N : Type*} [SMul N Y] [TopologicalSpace N] {f : N → M}
    (hg : IsInducing g) (hf : Continuous f) (hsmul : ∀ {c x}, g (c • x) = f c • g x) :
    ContinuousSMul N Y where
  continuous_smul := by
    simpa only [hg.continuous_iff, Function.comp_def, hsmul]
      using (hf.comp continuous_fst).smul <| hg.continuous.comp continuous_snd

Induced Continuous Scalar Multiplication via Action Homomorphism

Informal description

Let $N$ and $Y$ be types equipped with a scalar multiplication action of $N$ on $Y$ and topological structures. Suppose there exists a continuous function $f \colon N \to M$ and a map $g \colon Y \to X$ that is inducing (i.e., the topology on $Y$ is the coinduced topology from $X$ via $g$). If $g$ satisfies the compatibility condition $g(c \cdot x) = f(c) \cdot g(x)$ for all $c \in N$ and $x \in Y$, then the scalar multiplication action of $N$ on $Y$ is continuous.

SMulMemClass.continuousSMul instance

{S : Type*} [SetLike S X] [SMulMemClass S M X] (s : S) : ContinuousSMul M s

Full source

@[to_additive]
instance SMulMemClass.continuousSMul {S : Type*} [SetLike S X] [SMulMemClass S M X] (s : S) :
    ContinuousSMul M s :=
  IsInducing.subtypeVal.continuousSMul continuous_id rfl

Continuous Scalar Multiplication on Subsets Closed Under Scalar Multiplication

Informal description

For any subset $s$ of $X$ that is closed under scalar multiplication by $M$, the scalar multiplication operation $M \times s \to s$ is continuous when $s$ is equipped with the subspace topology.

Units.continuousSMul instance

: ContinuousSMul Mˣ X

Full source

@[to_additive]
instance Units.continuousSMul : ContinuousSMul Mˣ X :=
  IsInducing.id.continuousSMul Units.continuous_val rfl

Continuous Scalar Multiplication by Units of a Monoid

Informal description

For any monoid $M$ acting continuously on a topological space $X$, the scalar multiplication action of the group of units $M^\times$ on $X$ is also continuous.

MulAction.continuousSMul_compHom theorem

 {N : Type*} [TopologicalSpace N] [Monoid N] {f : N →* M} (hf : Continuous f) :
  letI : MulAction N X := MulAction.compHom _ f
  ContinuousSMul N X

Full source

/-- If an action is continuous, then composing this action with a continuous homomorphism gives
again a continuous action. -/
@[to_additive]
theorem MulAction.continuousSMul_compHom
    {N : Type*} [TopologicalSpace N] [Monoid N] {f : N →* M} (hf : Continuous f) :
    letI : MulAction N X := MulAction.compHom _ f
    ContinuousSMul N X := by
  let _ : MulAction N X := MulAction.compHom _ f
  exact ⟨(hf.comp continuous_fst).smul continuous_snd⟩

Continuity of Induced Scalar Multiplication via Continuous Homomorphism

Informal description

Let $M$ and $X$ be types with topological spaces, where $M$ is a monoid acting on $X$ via scalar multiplication. Given a monoid $N$ with a topological space and a continuous monoid homomorphism $f: N \to M$, the induced action of $N$ on $X$ (defined by $n \cdot x = f(n) \cdot x$) is continuous.

Submonoid.continuousSMul instance

{S : Submonoid M} : ContinuousSMul S X

Full source

@[to_additive]
instance Submonoid.continuousSMul {S : Submonoid M} : ContinuousSMul S X :=
  IsInducing.id.continuousSMul continuous_subtype_val rfl

Continuous Scalar Multiplication by Submonoids

Informal description

For any submonoid $S$ of a monoid $M$ acting continuously on a topological space $X$, the scalar multiplication action of $S$ on $X$ is continuous.

Subgroup.continuousSMul instance

{S : Subgroup M} : ContinuousSMul S X

Full source

@[to_additive]
instance Subgroup.continuousSMul {S : Subgroup M} : ContinuousSMul S X :=
  S.toSubmonoid.continuousSMul

Continuous Scalar Multiplication by Subgroups

Informal description

For any subgroup $S$ of a monoid $M$ acting continuously on a topological space $X$, the scalar multiplication action of $S$ on $X$ is continuous.

stabilizer_isOpen theorem

[DiscreteTopology X] (x : X) : IsOpen (MulAction.stabilizer M x : Set M)

Full source

/-- The stabilizer of a continuous group action on a discrete space is an open subgroup. -/
lemma stabilizer_isOpen [DiscreteTopology X] (x : X) : IsOpen (MulAction.stabilizer M x : Set M) :=
  IsOpen.preimage (f := fun g ↦ g • x) (by fun_prop) (isOpen_discrete {x})

Openness of Stabilizer Subgroup for Continuous Actions on Discrete Spaces

Informal description

Let $M$ be a topological monoid acting continuously on a discrete topological space $X$. For any element $x \in X$, the stabilizer subgroup $\text{stabilizer}_M(x) = \{m \in M \mid m \cdot x = x\}$ is an open subset of $M$.

Prod.continuousSMul instance

[SMul M X] [SMul M Y] [ContinuousSMul M X] [ContinuousSMul M Y] : ContinuousSMul M (X × Y)

Full source

@[to_additive]
instance Prod.continuousSMul [SMul M X] [SMul M Y] [ContinuousSMul M X] [ContinuousSMul M Y] :
    ContinuousSMul M (X × Y) :=
  ⟨(continuous_fst.smul (continuous_fst.comp continuous_snd)).prodMk
      (continuous_fst.smul (continuous_snd.comp continuous_snd))⟩

Continuous Scalar Multiplication on Product Spaces

Informal description

For any types $X$ and $Y$ with scalar multiplication actions by $M$, if the scalar multiplication is continuous on both $X$ and $Y$, then the scalar multiplication on the product space $X \times Y$ is also continuous.

instContinuousSMulForall instance

 {ι : Type*} {γ : ι → Type*} [∀ i, TopologicalSpace (γ i)] [∀ i, SMul M (γ i)] [∀ i, ContinuousSMul M (γ i)] :
  ContinuousSMul M (∀ i, γ i)

Full source

@[to_additive]
instance {ι : Type*} {γ : ι → Type*} [∀ i, TopologicalSpace (γ i)] [∀ i, SMul M (γ i)]
    [∀ i, ContinuousSMul M (γ i)] : ContinuousSMul M (∀ i, γ i) :=
  ⟨continuous_pi fun i =>
      (continuous_fst.smul continuous_snd).comp <|
        continuous_fst.prodMk ((continuous_apply i).comp continuous_snd)⟩

Continuous Scalar Multiplication on Product Spaces

Informal description

For any family of types $\{\gamma_i\}_{i \in \iota}$ where each $\gamma_i$ is equipped with a topological space and a scalar multiplication action by $M$, if the scalar multiplication is continuous on each $\gamma_i$, then the pointwise scalar multiplication on the product space $\prod_{i \in \iota} \gamma_i$ is also continuous.

continuousSMul_sInf theorem

{ts : Set (TopologicalSpace X)} (h : ∀ t ∈ ts, @ContinuousSMul M X _ _ t) : @ContinuousSMul M X _ _ (sInf ts)

Full source

@[to_additive]
theorem continuousSMul_sInf {ts : Set (TopologicalSpace X)}
    (h : ∀ t ∈ ts, @ContinuousSMul M X _ _ t) : @ContinuousSMul M X _ _ (sInf ts) :=
  -- Porting note: {} doesn't work because `sInf ts` isn't found by TC search. `(_)` finds it by
  -- unification instead.
  @ContinuousSMul.mk M X _ _ (_) <| by
      -- Porting note: needs `( :)`
      rw [← (@sInf_singleton _ _ ‹TopologicalSpace M›:)]
      exact
        continuous_sInf_rng.2 fun t ht =>
          continuous_sInf_dom₂ (Eq.refl _) ht
            (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))

Continuity of Scalar Multiplication under Infimum Topology

Informal description

Let $X$ be a type with a scalar multiplication action by $M$, and let $\{t_i\}_{i \in I}$ be a collection of topologies on $X$. If for each topology $t_i$ in the collection, the scalar multiplication operation $(•) : M × X → X$ is continuous with respect to $t_i$, then the scalar multiplication is also continuous with respect to the infimum topology $\bigwedge_{i \in I} t_i$ on $X$.

continuousSMul_iInf theorem

{ts' : ι → TopologicalSpace X} (h : ∀ i, @ContinuousSMul M X _ _ (ts' i)) : @ContinuousSMul M X _ _ (⨅ i, ts' i)

Full source

@[to_additive]
theorem continuousSMul_iInf {ts' : ι → TopologicalSpace X}
    (h : ∀ i, @ContinuousSMul M X _ _ (ts' i)) : @ContinuousSMul M X _ _ (⨅ i, ts' i) :=
  continuousSMul_sInf <| Set.forall_mem_range.mpr h

Continuity of Scalar Multiplication under Infimum of Topologies

Informal description

Let $X$ be a type with a scalar multiplication action by $M$, and let $\{t_i\}_{i \in \iota}$ be a family of topologies on $X$. If for each index $i \in \iota$, the scalar multiplication operation $(•) : M × X → X$ is continuous with respect to the topology $t_i$, then the scalar multiplication is also continuous with respect to the infimum topology $\bigwedge_{i \in \iota} t_i$ on $X$.

continuousSMul_inf theorem

 {t₁ t₂ : TopologicalSpace X} [@ContinuousSMul M X _ _ t₁] [@ContinuousSMul M X _ _ t₂] :
  @ContinuousSMul M X _ _ (t₁ ⊓ t₂)

Full source

@[to_additive]
theorem continuousSMul_inf {t₁ t₂ : TopologicalSpace X} [@ContinuousSMul M X _ _ t₁]
    [@ContinuousSMul M X _ _ t₂] : @ContinuousSMul M X _ _ (t₁ ⊓ t₂) := by
  rw [inf_eq_iInf]
  refine continuousSMul_iInf fun b => ?_
  cases b <;> assumption

Continuity of Scalar Multiplication under Infimum of Two Topologies

Informal description

Let $X$ be a type with a scalar multiplication action by $M$, and let $t_1$ and $t_2$ be two topologies on $X$. If the scalar multiplication operation $(•) : M × X → X$ is continuous with respect to both $t_1$ and $t_2$, then it is also continuous with respect to the infimum topology $t_1 \sqcap t_2$ on $X$.

AddTorsor.connectedSpace theorem

: ConnectedSpace P

Full source

/-- An `AddTorsor` for a connected space is a connected space. This is not an instance because
it loops for a group as a torsor over itself. -/
protected theorem AddTorsor.connectedSpace : ConnectedSpace P :=
  { isPreconnected_univ := by
      convert
        isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
          (continuous_id.vadd continuous_const).continuousOn
      rw [Set.image_univ, Equiv.range_eq_univ]
    toNonempty := inferInstance }

Connectedness of Additive Torsors Over Connected Spaces

Informal description

If $P$ is an additive torsor over a connected space, then $P$ itself is a connected space.

Mathlib.Topology.Algebra.MulAction

Main definitions

Main results