# mathlibdocumentation

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.

@[class]
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
@[class]
structure has_continuous_mul (M : Type u_5) [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
theorem continuous_mul {M : Type u_3} [has_mul M]  :
continuous (λ (p : M × M), (p.fst) * p.snd)

continuous (λ (p : M × M), p.fst + p.snd)

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

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

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

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

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

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

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

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

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

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

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

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

theorem tendsto.const_mul {α : Type u_1} {M : Type u_3} [has_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))

theorem tendsto.const_add {α : Type u_1} {M : Type u_3} [has_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))

theorem tendsto.add_const {α : Type u_1} {M : Type u_3} [has_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))

theorem tendsto.mul_const {α : Type u_1} {M : Type u_3} [has_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))

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

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

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

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

@[instance]

@[instance]
def prod.has_continuous_mul {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N]  :

theorem exists_open_nhds_one_split {M : Type u_3} [monoid M] {s : set M} :
s 𝓝 1(∃ (V : set M), 1 V ∀ (v : M), v V∀ (w : M), w Vv * w s)

theorem exists_open_nhds_zero_half {M : Type u_3} [add_monoid M] {s : set M} :
s 𝓝 0(∃ (V : set M), 0 V ∀ (v : M), v V∀ (w : M), w Vv + w s)

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

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

theorem exists_nhds_one_split4 {M : Type u_3} [monoid M] {u : set M} :
u 𝓝 1(∃ (V : set M) (H : V 𝓝 1), ∀ {v w s t : M}, v Vw Vs Vt V((v * w) * s) * t u)

theorem exists_nhds_zero_quarter {M : Type u_3} [add_monoid M] {u : set M} :
u 𝓝 0(∃ (V : set M) (H : V 𝓝 0), ∀ {v w s t : M}, v Vw Vs Vt Vv + w + s + t u)

theorem exists_open_nhds_zero_add_subset {M : Type u_3} [add_monoid M] {U : set M} :
U 𝓝 0(∃ (V : set M), 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.

theorem exists_open_nhds_one_mul_subset {M : Type u_3} [monoid M] {U : set M} :
U 𝓝 1(∃ (V : set M), 1 V V * V U)

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

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

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

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

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

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

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

S 𝓝 0

theorem submonoid.mem_nhds_one {M : Type u_3} [comm_monoid M] (S : submonoid M) :
S 𝓝 1

theorem tendsto_multiset_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} {f : β → α → M} {x : filter α} {a : β → M} (s : multiset β) :
(∀ (c : β), c sfilter.tendsto (f c) x (𝓝 (a c)))filter.tendsto (λ (b : α), (multiset.map (λ (c : β), f c b) s).sum) x (𝓝 s).sum)

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

theorem tendsto_finset_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} {f : β → α → M} {x : filter α} {a : β → M} (s : finset β) :
(∀ (c : β), c sfilter.tendsto (f c) x (𝓝 (a c)))filter.tendsto (λ (b : α), ∑ (c : β) in s, f c b) x (𝓝 (∑ (c : β) in s, a c))

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

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

theorem continuous_multiset_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} {f : β → α → M} (s : multiset β) :
(∀ (c : β), c scontinuous (f c))continuous (λ (a : α), (multiset.map (λ (c : β), f c a) s).sum)

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

theorem continuous_finset_sum {α : Type u_1} {β : Type u_2} {M : Type u_3} {f : β → α → M} (s : finset β) :
(∀ (c : β), c scontinuous (f c))continuous (λ (a : α), ∑ (c : β) in s, f c a)