Topological monoids - definitions

In this file we define two mixin typeclasses:

• ContinuousMul M says that the multiplication on M is continuous as a function on M × M;
• ContinuousAdd M says that the addition on M is continuous as a function on M × 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.

class ContinuousAdd (M : Type u_1) [TopologicalSpace M] [Add M] : Prop

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

class ContinuousMul (M : Type u_1) [TopologicalSpace M] [Mul M] : Prop

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

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.mul {M : Type u_1} [TopologicalSpace M] [Mul M] [ContinuousMul M] {α : Type u_2} {f g : α → M} {x : Filter α} {a b : M} (hf : Tendsto f x (nhds a)) (hg : Tendsto g x (nhds b)) : Tendsto (fun (x : α) => f x * g x) x (nhds (a * b))

theorem Filter.Tendsto.add {M : Type u_1} [TopologicalSpace M] [Add M] [ContinuousAdd M] {α : Type u_2} {f g : α → M} {x : Filter α} {a b : M} (hf : Tendsto f x (nhds a)) (hg : Tendsto g x (nhds b)) : Tendsto (fun (x : α) => f x + g x) x (nhds (a + b))

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 fun (x : X) => f x * g x

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 fun (x : X) => f x + g x

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 (fun (x : X) => f x * g x) 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 (fun (x : X) => f x + g x) 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 (fun (x : X) => f x * g x) 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 (fun (x : X) => f x + g x) 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 (fun (x : X) => f x * g x) s

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 (fun (x : X) => f x + g x) s