Topological monoids - definitions #
In this file we define two mixin typeclasses:
ContinuousMul Msays that the multiplication onMis continuous as a function onM ร M;ContinuousAdd Msays that the addition onMis continuous as a function onM ร M.
These classes are Prop-valued mixins,
i.e., they take data (TopologicalSpace, Mul/Add) as arguments
instead of extending typeclasses with these fields.
We also provide convenience dot notation lemmas like Filter.Tendsto.mul and ContinuousAt.add.
Basic hypothesis to talk about a topological additive monoid or a topological additive
semigroup. A topological additive monoid over M, for example, is obtained by requiring both the
instances AddMonoid M and ContinuousAdd M.
Continuity in only the left/right argument can be stated using
ContinuousConstVAdd ฮฑ ฮฑ/ContinuousConstVAdd ฮฑแตแตแต ฮฑ.
- continuous_add : Continuous fun (p : M ร M) => p.1 + p.2
Instances
Basic hypothesis to talk about a topological monoid or a topological semigroup.
A topological monoid over M, for example, is obtained by requiring both the instances Monoid M
and ContinuousMul M.
Continuity in only the left/right argument can be stated using
ContinuousConstSMul ฮฑ ฮฑ/ContinuousConstSMul ฮฑแตแตแต ฮฑ.
- continuous_mul : Continuous fun (p : M ร M) => p.1 * p.2
Instances
theorem
continuous_mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
Continuous fun (p : M ร M) => p.1 * p.2
theorem
continuous_add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
Continuous fun (p : M ร M) => p.1 + p.2
theorem
Filter.tendsto_of_div_tendsto_one
{ฮฑ : Type u_2}
{E : Type u_3}
[CommGroup E]
[TopologicalSpace E]
[ContinuousMul E]
{f g : ฮฑ โ E}
(m : E)
{x : Filter ฮฑ}
(hf : Tendsto f x (nhds m))
(hfg : Tendsto (g / f) x (nhds 1))
:
theorem
Filter.tendsto_of_sub_tendsto_zero
{ฮฑ : Type u_2}
{E : Type u_3}
[AddCommGroup E]
[TopologicalSpace E]
[ContinuousAdd E]
{f g : ฮฑ โ E}
(m : E)
{x : Filter ฮฑ}
(hf : Tendsto f x (nhds m))
(hfg : Tendsto (g - f) x (nhds 0))
:
theorem
Continuous.mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (f * g)
theorem
Continuous.fun_mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (i : X) => f i * g i
Eta-expanded form of Continuous.mul
theorem
Continuous.add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous (f + g)
theorem
Continuous.fun_add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (i : X) => f i + g i
theorem
ContinuousWithinAt.mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{s : Set X}
{x : X}
(hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g s x)
:
ContinuousWithinAt (f * g) s x
theorem
ContinuousWithinAt.fun_mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{s : Set X}
{x : X}
(hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g s x)
:
ContinuousWithinAt (fun (i : X) => f i * g i) s x
Eta-expanded form of ContinuousWithinAt.mul
theorem
ContinuousWithinAt.fun_add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{s : Set X}
{x : X}
(hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g s x)
:
ContinuousWithinAt (fun (i : X) => f i + g i) s x
theorem
ContinuousWithinAt.add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{s : Set X}
{x : X}
(hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g s x)
:
ContinuousWithinAt (f + g) s x
theorem
ContinuousAt.mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (f * g) x
theorem
ContinuousAt.fun_mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (i : X) => f i * g i) x
Eta-expanded form of ContinuousAt.mul
theorem
ContinuousAt.fun_add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (i : X) => f i + g i) x
theorem
ContinuousAt.add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (f + g) x
theorem
ContinuousOn.mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{s : Set X}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (f * g) s
theorem
ContinuousOn.fun_mul
{M : Type u_1}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{s : Set X}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (fun (i : X) => f i * g i) s
Eta-expanded form of ContinuousOn.mul
theorem
ContinuousOn.add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{s : Set X}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (f + g) s
theorem
ContinuousOn.fun_add
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{X : Type u_2}
[TopologicalSpace X]
{f g : X โ M}
{s : Set X}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (fun (i : X) => f i + g i) s