mathlib documentation

topology.algebra.monoid

Theory of topological monoids

In this file we define mixin classes has_continuous_mul and has_continuous_add. While in many applications the underlying type is a monoid (multiplicative or additive), we do not require this in the definitions.

source
@[class]
structure has_continuous_add (M : Type u_5) [topological_space M] [has_add M] :
Prop

Basic hypothesis to talk about a topological additive monoid or a topological additive semigroup. A topological additive monoid over α, for example, is obtained by requiring both the instances add_monoid α and has_continuous_add α.

Instances
source
@[class]
structure has_continuous_mul (M : Type u_5) [topological_space M] [has_mul M] :
Prop

Basic hypothesis to talk about a topological monoid or a topological semigroup. A topological monoid over α, for example, is obtained by requiring both the instances monoid α and has_continuous_mul α.

Instances
source
theorem continuous_mul {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] :
continuous (λ (p : M × M), (p.fst) * p.snd)

source
theorem continuous_add {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] :
continuous (λ (p : M × M), p.fst + p.snd)

source
theorem continuous.add {α : Type u_1} {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] [topological_space α] {f g : α → M} :
continuous f → continuous g → continuous (λ (x : α), f x + g x)

source
theorem continuous.mul {α : Type u_1} {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] [topological_space α] {f g : α → M} :
continuous f → continuous g → continuous (λ (x : α), (f x) * g x)

source
theorem continuous_add_left {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] (a : M) :
continuous (λ (b : M), a + b)

source
theorem continuous_mul_left {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] (a : M) :
continuous (λ (b : M), a * b)

source
theorem continuous_add_right {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] (a : M) :
continuous (λ (b : M), b + a)

source
theorem continuous_mul_right {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] (a : M) :
continuous (λ (b : M), b * a)

source
theorem continuous_on.add {α : Type u_1} {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] [topological_space α] {f g : α → M} {s : set α} :
continuous_on f s → continuous_on g s → continuous_on (λ (x : α), f x + g x) s

source
theorem continuous_on.mul {α : Type u_1} {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] [topological_space α] {f g : α → M} {s : set α} :
continuous_on f s → continuous_on g s → continuous_on (λ (x : α), (f x) * g x) s

source
theorem tendsto_add {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] {a b : M} :
filter.tendsto (λ (p : M × M), p.fst + p.snd) (𝓝 (a, b)) (𝓝 (a + b))

source
theorem tendsto_mul {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] {a b : M} :
filter.tendsto (λ (p : M × M), (p.fst) * p.snd) (𝓝 (a, b)) (𝓝 (a * b))

source
theorem filter.tendsto.add {α : Type u_1} {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] {f g : α → M} {x : filter α} {a b : M} :
filter.tendsto f x (𝓝 a) → filter.tendsto g x (𝓝 b) → filter.tendsto (λ (x : α), f x + g x) x (𝓝 (a + b))

source
theorem filter.tendsto.mul {α : Type u_1} {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] {f g : α → M} {x : filter α} {a b : M} :
filter.tendsto f x (𝓝 a) → filter.tendsto g x (𝓝 b) → filter.tendsto (λ (x : α), (f x) * g x) x (𝓝 (a * b))

source
theorem tendsto.const_mul {α : Type u_1} {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] (b : M) {c : M} {f : α → M} {l : filter α} :
filter.tendsto (λ (k : α), f k) l (𝓝 c) → filter.tendsto (λ (k : α), b * f k) l (𝓝 (b * c))

source
theorem tendsto.const_add {α : Type u_1} {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] (b : M) {c : M} {f : α → M} {l : filter α} :
filter.tendsto (λ (k : α), f k) l (𝓝 c) → filter.tendsto (λ (k : α), b + f k) l (𝓝 (b + c))

source
theorem tendsto.add_const {α : Type u_1} {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] (b : M) {c : M} {f : α → M} {l : filter α} :
filter.tendsto (λ (k : α), f k) l (𝓝 c) → filter.tendsto (λ (k : α), f k + b) l (𝓝 (c + b))

source
theorem tendsto.mul_const {α : Type u_1} {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] (b : M) {c : M} {f : α → M} {l : filter α} :
filter.tendsto (λ (k : α), f k) l (𝓝 c) → filter.tendsto (λ (k : α), (f k) * b) l (𝓝 (c * b))

source
theorem continuous_at.add {α : Type u_1} {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] [topological_space α] {f g : α → M} {x : α} :
continuous_at f x → continuous_at g x → continuous_at (λ (x : α), f x + g x) x

source
theorem continuous_at.mul {α : Type u_1} {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] [topological_space α] {f g : α → M} {x : α} :
continuous_at f x → continuous_at g x → continuous_at (λ (x : α), (f x) * g x) x

source
theorem continuous_within_at.add {α : Type u_1} {M : Type u_3} [topological_space M] [has_add M] [has_continuous_add M] [topological_space α] {f g : α → M} {s : set α} {x : α} :
continuous_within_at f s x → continuous_within_at g s x → continuous_within_at (λ (x : α), f x + g x) s x

source
theorem continuous_within_at.mul {α : Type u_1} {M : Type u_3} [topological_space M] [has_mul M] [has_continuous_mul M] [topological_space α] {f g : α → M} {s : set α} {x : α} :
continuous_within_at f s x → continuous_within_at g s x → continuous_within_at (λ (x : α), (f x) * g x) s x

source
@[instance]
def prod.has_continuous_add {M : Type u_3} {N : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] [topological_space N] [has_add N] [has_continuous_add N] :
has_continuous_add (M × N)

source
@[instance]
def prod.has_continuous_mul {M : Type u_3} {N : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] [topological_space N] [has_mul N] [has_continuous_mul N] :
has_continuous_mul (M × N)

source
theorem exists_open_nhds_one_split {M : Type u_3} [topological_space M] [monoid M] [has_continuous_mul M] {s : set M} :
s ∈ 𝓝 1 → (∃ (V : set M), is_open V ∧ 1 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s)

source
theorem exists_open_nhds_zero_half {M : Type u_3} [topological_space M] [add_monoid M] [has_continuous_add M] {s : set M} :
s ∈ 𝓝 0 → (∃ (V : set M), is_open V ∧ 0 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v + w ∈ s)

source
theorem exists_nhds_zero_half {M : Type u_3} [topological_space M] [add_monoid M] [has_continuous_add M] {s : set M} :
s ∈ 𝓝 0 → (∃ (V : set M) (H : V ∈ 𝓝 0), ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v + w ∈ s)

source
theorem exists_nhds_one_split {M : Type u_3} [topological_space M] [monoid M] [has_continuous_mul M] {s : set M} :
s ∈ 𝓝 1 → (∃ (V : set M) (H : V ∈ 𝓝 1), ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s)

source
theorem exists_nhds_one_split4 {M : Type u_3} [topological_space M] [monoid M] [has_continuous_mul M] {u : set M} :
u ∈ 𝓝 1 → (∃ (V : set M) (H : V ∈ 𝓝 1), ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → ((v * w) * s) * t ∈ u)

source
theorem exists_nhds_zero_quarter {M : Type u_3} [topological_space M] [add_monoid M] [has_continuous_add M] {u : set M} :
u ∈ 𝓝 0 → (∃ (V : set M) (H : V ∈ 𝓝 0), ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v + w + s + t ∈ u)

source
theorem exists_open_nhds_zero_add_subset {M : Type u_3} [topological_space M] [add_monoid M] [has_continuous_add M] {U : set M} :
U ∈ 𝓝 0 → (∃ (V : set M), is_open V ∧ 0 ∈ V ∧ V + V ⊆ U)

Given a open neighborhood U of 0 there is a open neighborhood V of 0 such that V + V ⊆ U.

source
theorem exists_open_nhds_one_mul_subset {M : Type u_3} [topological_space M] [monoid M] [has_continuous_mul M] {U : set M} :
U ∈ 𝓝 1 → (∃ (V : set M), is_open V ∧ 1 ∈ V ∧ V * V ⊆ U)

Given a neighborhood U of 1 there is an open neighborhood V of 1 such that VV ⊆ U.

source
theorem tendsto_list_prod {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [monoid M] [has_continuous_mul M] {f : β → α → M} {x : filter α} {a : β → M} (l : list β) :
(∀ (c : β), c ∈ l → filter.tendsto (f c) x (𝓝 (a c))) → filter.tendsto (λ (b : α), (list.map (λ (c : β), f c b) l).prod) x (𝓝 (list.map a l).prod)

source
theorem tendsto_list_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [add_monoid M] [has_continuous_add M] {f : β → α → M} {x : filter α} {a : β → M} (l : list β) :
(∀ (c : β), c ∈ l → filter.tendsto (f c) x (𝓝 (a c))) → filter.tendsto (λ (b : α), (list.map (λ (c : β), f c b) l).sum) x (𝓝 (list.map a l).sum)

source
theorem continuous_list_prod {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [monoid M] [has_continuous_mul M] [topological_space α] {f : β → α → M} (l : list β) :
(∀ (c : β), c ∈ l → continuous (f c)) → continuous (λ (a : α), (list.map (λ (c : β), f c a) l).prod)

source
theorem continuous_list_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [add_monoid M] [has_continuous_add M] [topological_space α] {f : β → α → M} (l : list β) :
(∀ (c : β), c ∈ l → continuous (f c)) → continuous (λ (a : α), (list.map (λ (c : β), f c a) l).sum)

source
theorem continuous_pow {M : Type u_3} [topological_space M] [monoid M] [has_continuous_mul M] (n : ℕ) :
continuous (λ (a : M), a ^ n)

source
theorem continuous.pow {α : Type u_1} {M : Type u_3} [topological_space M] [monoid M] [has_continuous_mul M] {f : α → M} [topological_space α] (h : continuous f) (n : ℕ) :
continuous (λ (b : α), f b ^ n)

source
theorem add_submonoid.mem_nhds_zero {M : Type u_3} [topological_space M] [add_comm_monoid M] (S : add_submonoid M) :
is_open ↑S → ↑S ∈ 𝓝 0

source
theorem submonoid.mem_nhds_one {M : Type u_3} [topological_space M] [comm_monoid M] (S : submonoid M) :
is_open ↑S → ↑S ∈ 𝓝 1

source
theorem tendsto_multiset_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : β → α → M} {x : filter α} {a : β → M} (s : multiset β) :
(∀ (c : β), c ∈ s → filter.tendsto (f c) x (𝓝 (a c))) → filter.tendsto (λ (b : α), (multiset.map (λ (c : β), f c b) s).sum) x (𝓝 (multiset.map a s).sum)

source
theorem tendsto_multiset_prod {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : β → α → M} {x : filter α} {a : β → M} (s : multiset β) :
(∀ (c : β), c ∈ s → filter.tendsto (f c) x (𝓝 (a c))) → filter.tendsto (λ (b : α), (multiset.map (λ (c : β), f c b) s).prod) x (𝓝 (multiset.map a s).prod)

source
theorem tendsto_finset_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : β → α → M} {x : filter α} {a : β → M} (s : finset β) :
(∀ (c : β), c ∈ s → filter.tendsto (f c) x (𝓝 (a c))) → filter.tendsto (λ (b : α), ∑ (c : β) in s, f c b) x (𝓝 (∑ (c : β) in s, a c))

source
theorem tendsto_finset_prod {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : β → α → M} {x : filter α} {a : β → M} (s : finset β) :
(∀ (c : β), c ∈ s → filter.tendsto (f c) x (𝓝 (a c))) → filter.tendsto (λ (b : α), ∏ (c : β) in s, f c b) x (𝓝 (∏ (c : β) in s, a c))

source
theorem continuous_multiset_prod {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [comm_monoid M] [has_continuous_mul M] [topological_space α] {f : β → α → M} (s : multiset β) :
(∀ (c : β), c ∈ s → continuous (f c)) → continuous (λ (a : α), (multiset.map (λ (c : β), f c a) s).prod)

source
theorem continuous_multiset_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [add_comm_monoid M] [has_continuous_add M] [topological_space α] {f : β → α → M} (s : multiset β) :
(∀ (c : β), c ∈ s → continuous (f c)) → continuous (λ (a : α), (multiset.map (λ (c : β), f c a) s).sum)

source
theorem continuous_finset_prod {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [comm_monoid M] [has_continuous_mul M] [topological_space α] {f : β → α → M} (s : finset β) :
(∀ (c : β), c ∈ s → continuous (f c)) → continuous (λ (a : α), ∏ (c : β) in s, f c a)

source
theorem continuous_finset_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} [topological_space M] [add_comm_monoid M] [has_continuous_add M] [topological_space α] {f : β → α → M} (s : finset β) :
(∀ (c : β), c ∈ s → continuous (f c)) → continuous (λ (a : α), ∑ (c : β) in s, f c a)