Continuous monoid action #
In this file we define class ContinuousSMul. We say ContinuousSMul M X if M acts on X and
the map (c, x) ↦ c • x is continuous on M × X. We reuse this class for topological
(semi)modules, vector spaces and algebras.
Main definitions #
ContinuousSMul M X: typeclass saying that the map(c, x) ↦ c • xis continuous onM × X;Units.continuousSMul: scalar multiplication byMˣis continuous when scalar multiplication byMis continuous. This allowsHomeomorph.smulto be used with on monoids withG = Mˣ.
-- Porting note: These have all moved
Homeomorph.smul_of_ne_zero: if a group with zeroG₀(e.g., a field) acts onXandc : G₀is a nonzero element ofG₀, then scalar multiplication bycis a homeomorphism ofX;Homeomorph.smul: scalar multiplication by an element of a groupGacting onXis a homeomorphism ofX.
Main results #
Besides homeomorphisms mentioned above, in this file we provide lemmas like Continuous.smul
or Filter.Tendsto.smul that provide dot-syntax access to ContinuousSMul.
class
ContinuousSMul
(M : Type u_1)
(X : Type u_2)
[SMul M X]
[TopologicalSpace M]
[TopologicalSpace X]
:
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.
- continuous_smul : Continuous fun (p : M × X) => p.1 • p.2
The scalar multiplication
(•)is continuous.
Instances
- AddGroup.continuousSMul_int
- AddMonoid.continuousSMul_nat
- BoundedSMul.continuousSMul
- Circle.instContinuousSMul
- ContinuousLinearMap.continuousSMul
- ContinuousMap.instContinuousSMulOfLocallyCompactSpace
- ContinuousMul.to_continuousSMul
- ContinuousMul.to_continuousSMul_op
- ContinuousMultilinearMap.instContinuousSMul
- ContinuousSMul.op
- ModuleFilterBasis.continuousSMul
- MulOpposite.continuousSMul
- NNReal.instContinuousSMulOfReal
- Prod.continuousSMul
- QuotientGroup.instContinuousSMul
- SMulMemClass.continuousSMul
- SeparationQuotient.instContinuousSMul
- Subgroup.continuousSMul
- Submodule.continuousSMul_quotient
- Submonoid.continuousSMul
- Units.continuousSMul
- WeakBilin.instContinuousSMul
- instContinuousSMulForall
- instContinuousSMulMatrix
- instContinuousSMulULift
theorem
ContinuousSMul.continuous_smul
{M : Type u_1}
{X : Type u_2}
:
∀ {inst : SMul M X} {inst_1 : TopologicalSpace M} {inst_2 : TopologicalSpace X} [self : ContinuousSMul M X],
Continuous fun (p : M × X) => p.1 • p.2
The scalar multiplication (•) is continuous.
class
ContinuousVAdd
(M : Type u_1)
(X : Type u_2)
[VAdd M X]
[TopologicalSpace M]
[TopologicalSpace X]
:
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.
- continuous_vadd : Continuous fun (p : M × X) => p.1 +ᵥ p.2
The additive action
(+ᵥ)is continuous.
Instances
- AddOpposite.continuousVAdd
- AddSubgroup.continuousVAdd
- AddSubmonoid.continuousVAdd
- AddUnits.continuousVAdd
- ContinuousAdd.to_continuousVAdd
- ContinuousAdd.to_continuousVAdd_op
- ContinuousMap.instContinuousVAddOfLocallyCompactSpace
- ContinuousVAdd.op
- NormedAddTorsor.to_continuousVAdd
- Prod.continuousVAdd
- QuotientAddGroup.instContinuousVAdd
- VAddMemClass.continuousVAdd
- instContinuousVAddForall
- instContinuousVAddULift
theorem
ContinuousVAdd.continuous_vadd
{M : Type u_1}
{X : Type u_2}
:
∀ {inst : VAdd M X} {inst_1 : TopologicalSpace M} {inst_2 : TopologicalSpace X} [self : ContinuousVAdd M X],
Continuous fun (p : M × X) => p.1 +ᵥ p.2
The additive action (+ᵥ) is continuous.
theorem
IsScalarTower.continuousSMul
{M : Type u_5}
(N : Type u_6)
{α : Type u_7}
[Monoid N]
[SMul M N]
[MulAction N α]
[SMul M α]
[IsScalarTower M N α]
[TopologicalSpace M]
[TopologicalSpace N]
[TopologicalSpace α]
[ContinuousSMul M N]
[ContinuousSMul N α]
:
ContinuousSMul M α
instance
instContinuousSMulULift
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
:
Equations
- ⋯ = ⋯
instance
instContinuousVAddULift
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
ContinuousSMul.continuousConstSMul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
ContinuousVAdd.continuousConstVAdd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
:
Equations
- ⋯ = ⋯
theorem
ContinuousSMul.induced
{R : Type u_5}
{α : Type u_6}
{β : Type u_7}
{F : Type u_8}
[FunLike F α β]
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[TopologicalSpace R]
[LinearMapClass F R α β]
[tβ : TopologicalSpace β]
[ContinuousSMul R β]
(f : F)
:
ContinuousSMul R α
theorem
Filter.Tendsto.smul
{M : Type u_1}
{X : Type u_2}
{α : Type u_4}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
{f : α → M}
{g : α → X}
{l : Filter α}
{c : M}
{a : X}
(hf : Filter.Tendsto f l (nhds c))
(hg : Filter.Tendsto g l (nhds a))
:
Filter.Tendsto (fun (x : α) => f x • g x) l (nhds (c • a))
theorem
Filter.Tendsto.vadd
{M : Type u_1}
{X : Type u_2}
{α : Type u_4}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
{f : α → M}
{g : α → X}
{l : Filter α}
{c : M}
{a : X}
(hf : Filter.Tendsto f l (nhds c))
(hg : Filter.Tendsto g l (nhds a))
:
Filter.Tendsto (fun (x : α) => f x +ᵥ g x) l (nhds (c +ᵥ a))
theorem
Filter.Tendsto.smul_const
{M : Type u_1}
{X : Type u_2}
{α : Type u_4}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
{f : α → M}
{l : Filter α}
{c : M}
(hf : Filter.Tendsto f l (nhds c))
(a : X)
:
Filter.Tendsto (fun (x : α) => f x • a) l (nhds (c • a))
theorem
Filter.Tendsto.vadd_const
{M : Type u_1}
{X : Type u_2}
{α : Type u_4}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
{f : α → M}
{l : Filter α}
{c : M}
(hf : Filter.Tendsto f l (nhds c))
(a : X)
:
Filter.Tendsto (fun (x : α) => f x +ᵥ a) l (nhds (c +ᵥ a))
theorem
ContinuousWithinAt.smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[SMul M X]
[ContinuousSMul M X]
{f : Y → M}
{g : Y → X}
{b : Y}
{s : Set Y}
(hf : ContinuousWithinAt f s b)
(hg : ContinuousWithinAt g s b)
:
ContinuousWithinAt (fun (x : Y) => f x • g x) s b
theorem
ContinuousWithinAt.vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[VAdd M X]
[ContinuousVAdd M X]
{f : Y → M}
{g : Y → X}
{b : Y}
{s : Set Y}
(hf : ContinuousWithinAt f s b)
(hg : ContinuousWithinAt g s b)
:
ContinuousWithinAt (fun (x : Y) => f x +ᵥ g x) s b
theorem
ContinuousAt.smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[SMul M X]
[ContinuousSMul M X]
{f : Y → M}
{g : Y → X}
{b : Y}
(hf : ContinuousAt f b)
(hg : ContinuousAt g b)
:
ContinuousAt (fun (x : Y) => f x • g x) b
theorem
ContinuousAt.vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[VAdd M X]
[ContinuousVAdd M X]
{f : Y → M}
{g : Y → X}
{b : Y}
(hf : ContinuousAt f b)
(hg : ContinuousAt g b)
:
ContinuousAt (fun (x : Y) => f x +ᵥ g x) b
theorem
ContinuousOn.smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[SMul M X]
[ContinuousSMul M X]
{f : Y → M}
{g : Y → X}
{s : Set Y}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (fun (x : Y) => f x • g x) s
theorem
ContinuousOn.vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[VAdd M X]
[ContinuousVAdd M X]
{f : Y → M}
{g : Y → X}
{s : Set Y}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (fun (x : Y) => f x +ᵥ g x) s
theorem
Continuous.smul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[SMul M X]
[ContinuousSMul M X]
{f : Y → M}
{g : Y → X}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (x : Y) => f x • g x
theorem
Continuous.vadd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[VAdd M X]
[ContinuousVAdd M X]
{f : Y → M}
{g : Y → X}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (x : Y) => f x +ᵥ g x
instance
ContinuousSMul.op
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
[SMul Mᵐᵒᵖ X]
[IsCentralScalar M X]
:
If a scalar action is central, then its right action is continuous when its left action is.
Equations
- ⋯ = ⋯
instance
ContinuousVAdd.op
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
[VAdd Mᵃᵒᵖ X]
[IsCentralVAdd M X]
:
If an additive action is central, then its right action is continuous when its left action is.
Equations
- ⋯ = ⋯
instance
MulOpposite.continuousSMul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
:
Equations
- ⋯ = ⋯
instance
AddOpposite.continuousVAdd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
:
Equations
- ⋯ = ⋯
theorem
Specializes.smul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
{a : M}
{b : M}
{x : X}
{y : X}
(h₁ : a ⤳ b)
(h₂ : x ⤳ y)
:
theorem
Specializes.vadd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
{a : M}
{b : M}
{x : X}
{y : X}
(h₁ : a ⤳ b)
(h₂ : x ⤳ y)
:
theorem
Inseparable.smul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
{a : M}
{b : M}
{x : X}
{y : X}
(h₁ : Inseparable a b)
(h₂ : Inseparable x y)
:
Inseparable (a • x) (b • y)
theorem
Inseparable.vadd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
{a : M}
{b : M}
{x : X}
{y : X}
(h₁ : Inseparable a b)
(h₂ : Inseparable x y)
:
Inseparable (a +ᵥ x) (b +ᵥ y)
theorem
IsCompact.smul_set
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
{k : Set M}
{u : Set X}
(hk : IsCompact k)
(hu : IsCompact u)
:
theorem
IsCompact.vadd_set
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
{k : Set M}
{u : Set X}
(hk : IsCompact k)
(hu : IsCompact u)
:
theorem
smul_set_closure_subset
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
(K : Set M)
(L : Set X)
:
theorem
vadd_set_closure_subset
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
(K : Set M)
(L : Set X)
:
theorem
IsInducing.continuousSMul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[SMul M X]
[ContinuousSMul M X]
{g : Y → X}
{N : Type u_5}
[SMul N Y]
[TopologicalSpace N]
{f : N → M}
(hg : IsInducing g)
(hf : Continuous f)
(hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x)
:
ContinuousSMul N Y
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.
theorem
IsInducing.continuousVAdd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[VAdd M X]
[ContinuousVAdd M X]
{g : Y → X}
{N : Type u_5}
[VAdd N Y]
[TopologicalSpace N]
{f : N → M}
(hg : IsInducing g)
(hf : Continuous f)
(hsmul : ∀ {c : N} {x : Y}, g (c +ᵥ x) = f c +ᵥ g x)
:
ContinuousVAdd N Y
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.
@[deprecated IsInducing.continuousSMul]
theorem
Inducing.continuousSMul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[SMul M X]
[ContinuousSMul M X]
{g : Y → X}
{N : Type u_5}
[SMul N Y]
[TopologicalSpace N]
{f : N → M}
(hg : IsInducing g)
(hf : Continuous f)
(hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x)
:
ContinuousSMul N Y
Alias of IsInducing.continuousSMul.
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.
instance
SMulMemClass.continuousSMul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[SMul M X]
[ContinuousSMul M X]
{S : Type u_5}
[SetLike S X]
[SMulMemClass S M X]
(s : S)
:
ContinuousSMul M ↥s
Equations
- ⋯ = ⋯
instance
VAddMemClass.continuousVAdd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[VAdd M X]
[ContinuousVAdd M X]
{S : Type u_5}
[SetLike S X]
[VAddMemClass S M X]
(s : S)
:
ContinuousVAdd M ↥s
Equations
- ⋯ = ⋯
instance
Units.continuousSMul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[Monoid M]
[MulAction M X]
[ContinuousSMul M X]
:
ContinuousSMul Mˣ X
Equations
- ⋯ = ⋯
instance
AddUnits.continuousVAdd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[AddMonoid M]
[AddAction M X]
[ContinuousVAdd M X]
:
ContinuousVAdd (AddUnits M) X
Equations
- ⋯ = ⋯
theorem
MulAction.continuousSMul_compHom
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[Monoid M]
[MulAction M X]
[ContinuousSMul M X]
{N : Type u_5}
[TopologicalSpace N]
[Monoid N]
{f : N →* M}
(hf : Continuous ⇑f)
:
ContinuousSMul N X
If an action is continuous, then composing this action with a continuous homomorphism gives again a continuous action.
theorem
AddAction.continuousVAdd_compHom
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[AddMonoid M]
[AddAction M X]
[ContinuousVAdd M X]
{N : Type u_5}
[TopologicalSpace N]
[AddMonoid N]
{f : N →+ M}
(hf : Continuous ⇑f)
:
ContinuousVAdd N X
instance
Submonoid.continuousSMul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[Monoid M]
[MulAction M X]
[ContinuousSMul M X]
{S : Submonoid M}
:
ContinuousSMul (↥S) X
Equations
- ⋯ = ⋯
instance
AddSubmonoid.continuousVAdd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[AddMonoid M]
[AddAction M X]
[ContinuousVAdd M X]
{S : AddSubmonoid M}
:
ContinuousVAdd (↥S) X
Equations
- ⋯ = ⋯
instance
Subgroup.continuousSMul
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[Group M]
[MulAction M X]
[ContinuousSMul M X]
{S : Subgroup M}
:
ContinuousSMul (↥S) X
Equations
- ⋯ = ⋯
instance
AddSubgroup.continuousVAdd
{M : Type u_1}
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[AddGroup M]
[AddAction M X]
[ContinuousVAdd M X]
{S : AddSubgroup M}
:
ContinuousVAdd (↥S) X
Equations
- ⋯ = ⋯
theorem
stabilizer_isOpen
(M : Type u_1)
{X : Type u_2}
[TopologicalSpace M]
[TopologicalSpace X]
[Group M]
[MulAction M X]
[ContinuousSMul M X]
[DiscreteTopology X]
(x : X)
:
IsOpen ↑(MulAction.stabilizer M x)
The stabilizer of a continuous group action on a discrete space is an open subgroup.
instance
Prod.continuousSMul
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[SMul M X]
[SMul M Y]
[ContinuousSMul M X]
[ContinuousSMul M Y]
:
ContinuousSMul M (X × Y)
Equations
- ⋯ = ⋯
instance
Prod.continuousVAdd
{M : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[TopologicalSpace M]
[TopologicalSpace X]
[TopologicalSpace Y]
[VAdd M X]
[VAdd M Y]
[ContinuousVAdd M X]
[ContinuousVAdd M Y]
:
ContinuousVAdd M (X × Y)
Equations
- ⋯ = ⋯
instance
instContinuousSMulForall
{M : Type u_1}
[TopologicalSpace M]
{ι : Type u_5}
{γ : ι → Type u_6}
[(i : ι) → TopologicalSpace (γ i)]
[(i : ι) → SMul M (γ i)]
[∀ (i : ι), ContinuousSMul M (γ i)]
:
ContinuousSMul M ((i : ι) → γ i)
Equations
- ⋯ = ⋯
instance
instContinuousVAddForall
{M : Type u_1}
[TopologicalSpace M]
{ι : Type u_5}
{γ : ι → Type u_6}
[(i : ι) → TopologicalSpace (γ i)]
[(i : ι) → VAdd M (γ i)]
[∀ (i : ι), ContinuousVAdd M (γ i)]
:
ContinuousVAdd M ((i : ι) → γ i)
Equations
- ⋯ = ⋯
theorem
continuousSMul_sInf
{M : Type u_2}
{X : Type u_3}
[TopologicalSpace M]
[SMul M X]
{ts : Set (TopologicalSpace X)}
(h : ∀ t ∈ ts, ContinuousSMul M X)
:
ContinuousSMul M X
theorem
continuousVAdd_sInf
{M : Type u_2}
{X : Type u_3}
[TopologicalSpace M]
[VAdd M X]
{ts : Set (TopologicalSpace X)}
(h : ∀ t ∈ ts, ContinuousVAdd M X)
:
ContinuousVAdd M X
theorem
continuousSMul_iInf
{ι : Sort u_1}
{M : Type u_2}
{X : Type u_3}
[TopologicalSpace M]
[SMul M X]
{ts' : ι → TopologicalSpace X}
(h : ∀ (i : ι), ContinuousSMul M X)
:
ContinuousSMul M X
theorem
continuousVAdd_iInf
{ι : Sort u_1}
{M : Type u_2}
{X : Type u_3}
[TopologicalSpace M]
[VAdd M X]
{ts' : ι → TopologicalSpace X}
(h : ∀ (i : ι), ContinuousVAdd M X)
:
ContinuousVAdd M X
theorem
continuousSMul_inf
{M : Type u_2}
{X : Type u_3}
[TopologicalSpace M]
[SMul M X]
{t₁ : TopologicalSpace X}
{t₂ : TopologicalSpace X}
[ContinuousSMul M X]
[ContinuousSMul M X]
:
ContinuousSMul M X
theorem
continuousVAdd_inf
{M : Type u_2}
{X : Type u_3}
[TopologicalSpace M]
[VAdd M X]
{t₁ : TopologicalSpace X}
{t₂ : TopologicalSpace X}
[ContinuousVAdd M X]
[ContinuousVAdd M X]
:
ContinuousVAdd M X
theorem
AddTorsor.connectedSpace
(G : Type u_1)
(P : Type u_2)
[AddGroup G]
[AddTorsor G P]
[TopologicalSpace G]
[PreconnectedSpace G]
[TopologicalSpace P]
[ContinuousVAdd G P]
:
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.