Topological monoids - definitions

In this file we define three 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.
• SeparatelyContinuousMul M says that the multiplication on M is continuous in each argument separately. This is strictly weaker than ContinuousMul M, but arises frequently in practice in functional analysis where one often considers topologies weaker than the norm topology. In these topologies it is frequently the case that the multiplication is not jointly continuous, but is continuous in each argument separately.

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 each argument separately can be stated using SeparatelyContinuousAdd α. If one wants only continuity in either the left or right argument, but not both one can use 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 each argument separately can be stated using SeparatelyContinuousMul α. If one wants only continuity in either the left or right argument, but not both one can use ContinuousConstSMul α α/ContinuousConstSMul αᵐᵒᵖ α.

• continuous_mul : Continuous fun (p : M × M) => p.1 * p.2

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

A type class encoding that addition is continuous in each argument. This is weaker than ContinuousAdd.

• continuous_const_add {a : M} : Continuous fun (x : M) => a + x
• continuous_add_const {a : M} : Continuous fun (x : M) => x + a

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

A type class encoding that addition is continuous in each argument. This is weaker than ContinuousMul.

• continuous_const_mul {a : M} : Continuous fun (x : M) => a * x
• continuous_mul_const {a : M} : Continuous fun (x : M) => x * a

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 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)) : Tendsto g x (nhds m)

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)) : Tendsto g x (nhds m)

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.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 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 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.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

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

instance instSeparatelyContinuousMulOfContinuousMul {M : Type u_1} [TopologicalSpace M] [Mul M] [ContinuousMul M] : SeparatelyContinuousMul M

instance instSeparatelyContinuousAddOfContinuousAdd {M : Type u_1} [TopologicalSpace M] [Add M] [ContinuousAdd M] : SeparatelyContinuousAdd M

theorem continuous_const_mul {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] (m : M) : Continuous fun (x : M) => m * x

theorem continuous_const_add {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] (m : M) : Continuous fun (x : M) => m + x

theorem continuous_mul_const {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] (m : M) : Continuous fun (x : M) => x * m

theorem continuous_add_const {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] (m : M) : Continuous fun (x : M) => x + m

theorem Filter.Tendsto.const_mul {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {α : Type u_2} {f : α → M} {x : Filter α} {a : M} (b : M) (hf : Tendsto f x (nhds a)) : Tendsto (fun (x : α) => b * f x) x (nhds (b * a))

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

theorem Filter.Tendsto.mul_const {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {α : Type u_2} {f : α → M} {x : Filter α} {a : M} (b : M) (hf : Tendsto f x (nhds a)) : Tendsto (fun (x : α) => f x * b) x (nhds (a * b))

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

theorem Continuous.mul_const {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {X : Type u_2} [TopologicalSpace X] {f : X → M} (hf : Continuous f) (b : M) : Continuous fun (x : X) => f x * b

theorem Continuous.add_const {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {X : Type u_2} [TopologicalSpace X] {f : X → M} (hf : Continuous f) (b : M) : Continuous fun (x : X) => f x + b

theorem Continuous.const_mul {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {X : Type u_2} [TopologicalSpace X] {f : X → M} (hf : Continuous f) (b : M) : Continuous fun (x : X) => b * f x

theorem Continuous.const_add {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {X : Type u_2} [TopologicalSpace X] {f : X → M} (hf : Continuous f) (b : M) : Continuous fun (x : X) => b + f x

theorem ContinuousWithinAt.mul_const {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (b : M) : ContinuousWithinAt (fun (x : X) => f x * b) s x

theorem ContinuousWithinAt.add_const {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (b : M) : ContinuousWithinAt (fun (x : X) => f x + b) s x

theorem ContinuousWithinAt.const_mul {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (b : M) : ContinuousWithinAt (fun (x : X) => b * f x) s x

theorem ContinuousWithinAt.const_add {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (b : M) : ContinuousWithinAt (fun (x : X) => b + f x) s x

theorem ContinuousAt.mul_const {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {x : X} (hf : ContinuousAt f x) (b : M) : ContinuousAt (fun (x : X) => f x * b) x

theorem ContinuousAt.add_const {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {x : X} (hf : ContinuousAt f x) (b : M) : ContinuousAt (fun (x : X) => f x + b) x

theorem ContinuousAt.const_mul {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {x : X} (hf : ContinuousAt f x) (b : M) : ContinuousAt (fun (x : X) => b * f x) x

theorem ContinuousAt.const_add {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {x : X} (hf : ContinuousAt f x) (b : M) : ContinuousAt (fun (x : X) => b + f x) x

theorem ContinuousOn.mul_const {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {s : Set X} (hf : ContinuousOn f s) (b : M) : ContinuousOn (fun (x : X) => f x * b) s

theorem ContinuousOn.add_const {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {s : Set X} (hf : ContinuousOn f s) (b : M) : ContinuousOn (fun (x : X) => f x + b) s

theorem ContinuousOn.const_mul {M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {s : Set X} (hf : ContinuousOn f s) (b : M) : ContinuousOn (fun (x : X) => b * f x) s

theorem ContinuousOn.const_add {M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {X : Type u_2} [TopologicalSpace X] {f : X → M} {s : Set X} (hf : ContinuousOn f s) (b : M) : ContinuousOn (fun (x : X) => b + f x) s