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]
- continuous_add : continuous (λ (p : M × M), p.fst + p.snd)
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
- has_continuous_add_of_discrete_topology
- topological_add_group.to_has_continuous_add
- add_group_with_zero_nhd.has_continuous_add
- topological_semiring.to_has_continuous_add
- topological_ring.to_has_continuous_add
- normed_top_monoid
- prod.has_continuous_add
- additive.has_continuous_add
- ennreal.has_continuous_add
@[class]
- continuous_mul : continuous (λ (p : M × M), (p.fst) * p.snd)
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 α.
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)
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)
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}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : α), f x + g x)
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}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : α), (f x) * g x)
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)
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)
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)
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)
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 α}
(hf : continuous_on f s)
(hg : continuous_on g s) :
continuous_on (λ (x : α), f x + g x) s
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 α}
(hf : continuous_on f s)
(hg : continuous_on g s) :
continuous_on (λ (x : α), (f x) * g x) s
theorem
tendsto_add
{M : Type u_3}
[topological_space M]
[has_add M]
[has_continuous_add M]
{a b : M} :
theorem
tendsto_mul
{M : Type u_3}
[topological_space M]
[has_mul M]
[has_continuous_mul M]
{a b : M} :
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}
(hf : filter.tendsto f x (𝓝 a))
(hg : filter.tendsto g x (𝓝 b)) :
filter.tendsto (λ (x : α), f x + g x) x (𝓝 (a + b))
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}
(hf : filter.tendsto f x (𝓝 a))
(hg : filter.tendsto g x (𝓝 b)) :
filter.tendsto (λ (x : α), (f x) * g x) x (𝓝 (a * b))
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 α}
(h : 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}
[topological_space M]
[has_add M]
[has_continuous_add M]
(b : M)
{c : M}
{f : α → M}
{l : filter α}
(h : 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}
[topological_space M]
[has_add M]
[has_continuous_add M]
(b : M)
{c : M}
{f : α → M}
{l : filter α}
(h : 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}
[topological_space M]
[has_mul M]
[has_continuous_mul M]
(b : M)
{c : M}
{f : α → M}
{l : filter α}
(h : 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}
[topological_space M]
[has_add M]
[has_continuous_add M]
[topological_space α]
{f g : α → M}
{x : α}
(hf : continuous_at f x)
(hg : continuous_at g x) :
continuous_at (λ (x : α), f x + g x) x
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 : α}
(hf : continuous_at f x)
(hg : continuous_at g x) :
continuous_at (λ (x : α), (f x) * g x) x
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 : α}
(hf : continuous_within_at f s x)
(hg : continuous_within_at g s x) :
continuous_within_at (λ (x : α), f x + g x) s x
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 : α}
(hf : continuous_within_at f s x)
(hg : continuous_within_at g s x) :
continuous_within_at (λ (x : α), (f x) * g x) s x
@[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)
@[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)
@[instance]
def
has_continuous_mul_of_discrete_topology
{N : Type u_4}
[topological_space N]
[has_mul N]
[discrete_topology N] :
@[instance]
def
has_continuous_add_of_discrete_topology
{N : Type u_4}
[topological_space N]
[has_add N]
[discrete_topology N] :
theorem
has_continuous_add.of_nhds_zero
{M : Type (max u_1 u_2)}
[add_monoid M]
[topological_space M]
(hmul : filter.tendsto (function.uncurry has_add.add) (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0))
(hleft : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x₀ + x) (𝓝 0))
(hright : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x + x₀) (𝓝 0)) :
theorem
has_continuous_mul.of_nhds_one
{M : Type (max u_1 u_2)}
[monoid M]
[topological_space M]
(hmul : filter.tendsto (function.uncurry has_mul.mul) (𝓝 1 ×ᶠ 𝓝 1) (𝓝 1))
(hleft : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x₀ * x) (𝓝 1))
(hright : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x * x₀) (𝓝 1)) :
theorem
has_continuous_mul_of_comm_of_nhds_one
(M : Type (max u_1 u_2))
[comm_monoid M]
[topological_space M]
(hmul : filter.tendsto (function.uncurry has_mul.mul) (𝓝 1 ×ᶠ 𝓝 1) (𝓝 1))
(hleft : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x₀ * x) (𝓝 1)) :
theorem
has_continuous_add_of_comm_of_nhds_zero
(M : Type (max u_1 u_2))
[add_comm_monoid M]
[topological_space M]
(hmul : filter.tendsto (function.uncurry has_add.add) (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0))
(hleft : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x₀ + x) (𝓝 0)) :
theorem
exists_open_nhds_zero_half
{M : Type u_3}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{s : set M}
(hs : s ∈ 𝓝 0) :
theorem
exists_nhds_zero_half
{M : Type u_3}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{s : set M}
(hs : s ∈ 𝓝 0) :
theorem
exists_nhds_one_split
{M : Type u_3}
[topological_space M]
[monoid M]
[has_continuous_mul M]
{s : set M}
(hs : s ∈ 𝓝 1) :
theorem
exists_nhds_zero_quarter
{M : Type u_3}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{u : set M}
(hu : u ∈ 𝓝 0) :
theorem
exists_open_nhds_zero_add_subset
{M : Type u_3}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{U : set M}
(hU : U ∈ 𝓝 0) :
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}
[topological_space M]
[monoid M]
[has_continuous_mul M]
{U : set M}
(hU : U ∈ 𝓝 1) :
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}
[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)
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)
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 β)
(h : ∀ (c : β), c ∈ l → continuous (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}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
[topological_space α]
{f : β → α → M}
(l : list β)
(h : ∀ (c : β), c ∈ l → continuous (f c)) :
continuous (λ (a : α), (list.map (λ (c : β), f c a) l).sum)
theorem
continuous_pow
{M : Type u_3}
[topological_space M]
[monoid M]
[has_continuous_mul M]
(n : ℕ) :
continuous (λ (a : M), a ^ n)
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)
theorem
add_submonoid.mem_nhds_zero
{M : Type u_3}
[topological_space M]
[add_comm_monoid M]
(S : add_submonoid M)
(oS : is_open ↑S) :
theorem
submonoid.mem_nhds_one
{M : Type u_3}
[topological_space M]
[comm_monoid M]
(S : submonoid M)
(oS : is_open ↑S) :
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)
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)
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))
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))
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)
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)
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)
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)
@[instance]
def
additive.has_continuous_add
{M : Type u_1}
[h : topological_space M]
[has_mul M]
[has_continuous_mul M] :
@[instance]
def
multiplicative.has_continuous_mul
{M : Type u_1}
[h : topological_space M]
[has_add M]
[has_continuous_add M] :