doc-next-gen

Mathlib.Topology.Algebra.Monoid.Defs

Module docstring

{"# 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. "}

ContinuousAdd structure
(M : Type*) [TopologicalSpace M] [Add M]
Full source 
/-- 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 αᵐᵒᵖ α`. -/
class ContinuousAdd (M : Type*) [TopologicalSpace M] [Add M] : Prop where
  continuous_add : Continuous fun p : M × M => p.1 + p.2
Continuous addition on a topological space
Informal description
The structure `ContinuousAdd M` asserts that the addition operation on a topological space `M` equipped with an addition is continuous as a function from `M × M` to `M`.
ContinuousMul structure
(M : Type*) [TopologicalSpace M] [Mul M]
Full source 
/-- 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 αᵐᵒᵖ α`. -/
@[to_additive]
class ContinuousMul (M : Type*) [TopologicalSpace M] [Mul M] : Prop where
  continuous_mul : Continuous fun p : M × M => p.1 * p.2
Continuous multiplication in a topological space
Informal description
A structure asserting that the multiplication operation on a topological space $M$ is continuous, where continuity is with respect to the product topology on $M \times M$.
continuous_mul theorem
: Continuous fun p : M × M => p.1 * p.2
Full source 
@[to_additive (attr := continuity, fun_prop)]
theorem continuous_mul : Continuous fun p : M × M => p.1 * p.2 :=
  ContinuousMul.continuous_mul
Continuity of multiplication in a topological monoid
Informal description
For a topological space $M$ equipped with a multiplication operation, the multiplication map $M \times M \to M$ defined by $(x, y) \mapsto x * y$ is continuous.
Filter.Tendsto.mul theorem
{α : Type*} {f g : α → M} {x : Filter α} {a b : M} (hf : Tendsto f x (𝓝 a)) (hg : Tendsto g x (𝓝 b)) : Tendsto (fun x ↦ f x * g x) x (𝓝 (a * b))
Full source 
@[to_additive]
theorem Filter.Tendsto.mul {α : Type*} {f g : α → M} {x : Filter α} {a b : M}
    (hf : Tendsto f x (𝓝 a)) (hg : Tendsto g x (𝓝 b)) : Tendsto (fun x ↦ f x * g x) x (𝓝 (a * b)) :=
  (continuous_mul.tendsto _).comp (hf.prodMk_nhds hg)
Limit of Pointwise Product in Topological Monoid
Informal description
Let $M$ be a topological space with a continuous multiplication operation, and let $\alpha$ be a type. For functions $f, g : \alpha \to M$ and a filter $x$ on $\alpha$, if $f$ tends to $a \in M$ along $x$ and $g$ tends to $b \in M$ along $x$, then the pointwise product function $x \mapsto f(x) * g(x)$ tends to $a * b$ along $x$. In symbols: \[ f \underset{x}{\to} a \text{ and } g \underset{x}{\to} b \implies (f \cdot g) \underset{x}{\to} (a \cdot b) \] where $\underset{x}{\to}$ denotes convergence in the neighborhood filters.
Continuous.mul theorem
(hf : Continuous f) (hg : Continuous g) : Continuous fun x => f x * g x
Full source 
@[to_additive (attr := continuity, fun_prop)]
theorem Continuous.mul (hf : Continuous f) (hg : Continuous g) :
    Continuous fun x => f x * g x :=
  continuous_mul.comp₂ hf hg
Continuity of Pointwise Product of Continuous Functions
Informal description
Let $M$ be a topological space with a continuous multiplication operation, and let $X$ be another topological space. For any continuous functions $f, g \colon X \to M$, the function $x \mapsto f(x) * g(x)$ is continuous.
ContinuousWithinAt.mul theorem
(hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun x => f x * g x) s x
Full source 
@[to_additive]
theorem ContinuousWithinAt.mul (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
    ContinuousWithinAt (fun x => f x * g x) s x :=
  Filter.Tendsto.mul hf hg
Continuity of Pointwise Product Within a Subset
Informal description
Let $M$ be a topological space with a continuous multiplication operation, and let $X$ be another topological space. For functions $f, g : X \to M$, a point $x \in X$, and a subset $s \subseteq X$, if $f$ is continuous at $x$ within $s$ and $g$ is continuous at $x$ within $s$, then the pointwise product function $x \mapsto f(x) \cdot g(x)$ is also continuous at $x$ within $s$. In symbols: \[ f \text{ continuous at } x \text{ within } s \text{ and } g \text{ continuous at } x \text{ within } s \implies (f \cdot g) \text{ continuous at } x \text{ within } s \]
ContinuousAt.mul theorem
(hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun x => f x * g x) x
Full source 
@[to_additive (attr := fun_prop)]
theorem ContinuousAt.mul (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
    ContinuousAt (fun x => f x * g x) x :=
  Filter.Tendsto.mul hf hg
Continuity of Pointwise Product at a Point
Informal description
Let $M$ be a topological space with a continuous multiplication operation, and let $X$ be another topological space. For functions $f, g \colon X \to M$ and a point $x \in X$, if $f$ is continuous at $x$ and $g$ is continuous at $x$, then the pointwise product function $x \mapsto f(x) \cdot g(x)$ is continuous at $x$. In symbols: \[ \text{ContinuousAt}(f, x) \text{ and } \text{ContinuousAt}(g, x) \implies \text{ContinuousAt}(x \mapsto f(x) \cdot g(x), x) \]
ContinuousOn.mul 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.mul (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun x => f x * g x) s := fun x hx ↦
  (hf x hx).mul (hg x hx)
Continuity of Pointwise Product on a Subset
Informal description
Let $M$ be a topological space with a continuous multiplication operation, and let $X$ be another topological space. For functions $f, g : X \to M$ and a subset $s \subseteq X$, if $f$ is continuous on $s$ and $g$ is continuous on $s$, then the pointwise product function $x \mapsto f(x) \cdot g(x)$ is also continuous on $s$. In symbols: \[ f \text{ continuous on } s \text{ and } g \text{ continuous on } s \implies (f \cdot g) \text{ continuous on } s \]