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
theorem continuous_zero {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_zero M] :
continuous 0
source
theorem continuous_one {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_one M] :
continuous 1
source
@[class]
structure has_continuous_add (M : Type u) [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 M, for example, is obtained by requiring both the instances add_monoid M and has_continuous_add M.

Instances
source
@[class]
structure has_continuous_mul (M : Type u) [topological_space M] [has_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 has_continuous_mul M.

Instances
source
theorem continuous_mul {M : Type u_4} [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_4} [topological_space M] [has_add M] [has_continuous_add M] :
continuous (λ (p : M × M), p.fst + p.snd)
source
theorem continuous.add {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_add M] [has_continuous_add M] {f g : X → M} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : X), f x + g x)
source
theorem continuous.mul {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_mul M] [has_continuous_mul M] {f g : X → M} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : X), (f x) * g x)
source
theorem continuous_add_left {M : Type u_4} [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_4} [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_4} [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_4} [topological_space M] [has_mul M] [has_continuous_mul M] (a : M) :
continuous (λ (b : M), b * a)
source
theorem continuous_on.add {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_add M] [has_continuous_add M] {f g : X → M} {s : set X} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : X), f x + g x) s
source
theorem continuous_on.mul {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_mul M] [has_continuous_mul M] {f g : X → M} {s : set X} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : X), (f x) * g x) s
source
theorem tendsto_add {M : Type u_4} [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_4} [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_2} {M : Type u_4} [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))
source
theorem filter.tendsto.mul {α : Type u_2} {M : Type u_4} [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))
source
theorem filter.tendsto.const_add {α : Type u_2} {M : Type u_4} [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))
source
theorem filter.tendsto.const_mul {α : Type u_2} {M : Type u_4} [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))
source
theorem filter.tendsto.mul_const {α : Type u_2} {M : Type u_4} [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))
source
theorem filter.tendsto.add_const {α : Type u_2} {M : Type u_4} [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))
source
theorem continuous_at.add {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_add M] [has_continuous_add M] {f g : X → M} {x : X} (hf : continuous_at f x) (hg : continuous_at g x) :
continuous_at (λ (x : X), f x + g x) x
source
theorem continuous_at.mul {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_mul M] [has_continuous_mul M] {f g : X → M} {x : X} (hf : continuous_at f x) (hg : continuous_at g x) :
continuous_at (λ (x : X), (f x) * g x) x
source
theorem continuous_within_at.add {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_add M] [has_continuous_add M] {f g : X → M} {s : set X} {x : X} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_within_at (λ (x : X), f x + g x) s x
source
theorem continuous_within_at.mul {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_mul M] [has_continuous_mul M] {f g : X → M} {s : set X} {x : X} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_within_at (λ (x : X), (f x) * g x) s x
source
@[instance]
def prod.has_continuous_add {M : Type u_4} {N : Type u_5} [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_4} {N : Type u_5} [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
@[instance]
def pi.has_continuous_mul {ι : Type u_1} {C : ι → Type u_2} [Π (i : ι), topological_space (C i)] [Π (i : ι), has_mul (C i)] [∀ (i : ι), has_continuous_mul (C i)] :
has_continuous_mul (Π (i : ι), C i)
source
@[instance]
def pi.has_continuous_add {ι : Type u_1} {C : ι → Type u_2} [Π (i : ι), topological_space (C i)] [Π (i : ι), has_add (C i)] [∀ (i : ι), has_continuous_add (C i)] :
has_continuous_add (Π (i : ι), C i)
source
@[instance]
def pi.has_continuous_mul' {ι : Type u_1} {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] :
has_continuous_mul (ι → M)

A version of pi.has_continuous_mul for non-dependent functions. It is needed because sometimes Lean fails to use pi.has_continuous_mul for non-dependent functions.

source
@[instance]
def pi.has_continuous_add' {ι : Type u_1} {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] :
has_continuous_add (ι → M)

A version of pi.has_continuous_add for non-dependent functions. It is needed because sometimes Lean fails to use pi.has_continuous_add for non-dependent functions.

source
@[instance]
def has_continuous_mul_of_discrete_topology {N : Type u_5} [topological_space N] [has_mul N] [discrete_topology N] :
has_continuous_mul N
source
@[instance]
def has_continuous_add_of_discrete_topology {N : Type u_5} [topological_space N] [has_add N] [discrete_topology N] :
has_continuous_add N
source
theorem has_continuous_add.of_nhds_zero {M : Type u} [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)) :
has_continuous_add M
source
theorem has_continuous_mul.of_nhds_one {M : Type u} [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)) :
has_continuous_mul M
source
theorem has_continuous_mul_of_comm_of_nhds_one (M : Type u) [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)) :
has_continuous_mul M
source
theorem has_continuous_add_of_comm_of_nhds_zero (M : Type u) [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)) :
has_continuous_add M
source
theorem add_submonoid.top_closure_add_self_subset {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] (s : add_submonoid M) :
closure ↑s + closure ↑s ⊆ closure ↑s
source
theorem submonoid.top_closure_mul_self_subset {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (s : submonoid M) :
(closure ↑s) * closure ↑s ⊆ closure ↑s
source
theorem add_submonoid.top_closure_add_self_eq {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] (s : add_submonoid M) :
closure ↑s + closure ↑s = closure ↑s
source
theorem submonoid.top_closure_mul_self_eq {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (s : submonoid M) :
(closure ↑s) * closure ↑s = closure ↑s
source
def submonoid.topological_closure {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (s : submonoid M) :
submonoid M

The (topological-space) closure of a submonoid of a space M with has_continuous_mul is itself a submonoid.

Equations
source
def add_submonoid.topological_closure {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] (s : add_submonoid M) :
add_submonoid M

The (topological-space) closure of an additive submonoid of a space M with has_continuous_add is itself an additive submonoid.

source
@[instance]
def submonoid.topological_closure_has_continuous_mul {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (s : submonoid M) :
has_continuous_mul ↥(s.topological_closure)
source
@[instance]
def add_submonoid.topological_closure_has_continuous_add {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] (s : add_submonoid M) :
has_continuous_add ↥(s.topological_closure)
source
theorem submonoid.submonoid_topological_closure {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (s : submonoid M) :
s ≤ s.topological_closure
source
theorem submonoid.is_closed_topological_closure {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (s : submonoid M) :
is_closed ↑(s.topological_closure)
source
theorem submonoid.topological_closure_minimal {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (s : submonoid M) {t : submonoid M} (h : s ≤ t) (ht : is_closed ↑t) :
s.topological_closure ≤ t
source
theorem exists_open_nhds_one_split {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {s : set M} (hs : 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_4} [topological_space M] [add_monoid M] [has_continuous_add M] {s : set M} (hs : 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_4} [topological_space M] [add_monoid M] [has_continuous_add M] {s : set M} (hs : 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_4} [topological_space M] [monoid M] [has_continuous_mul M] {s : set M} (hs : 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_4} [topological_space M] [monoid M] [has_continuous_mul M] {u : set M} (hu : 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_4} [topological_space M] [add_monoid M] [has_continuous_add M] {u : set M} (hu : 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_4} [topological_space M] [add_monoid M] [has_continuous_add M] {U : set M} (hU : 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_4} [topological_space M] [monoid M] [has_continuous_mul M] {U : set M} (hU : 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_4} [topological_space M] [monoid M] [has_continuous_mul M] {f : ι → α → M} {x : filter α} {a : ι → M} (l : list ι) :
(∀ (i : ι), i ∈ l → filter.tendsto (f i) x (𝓝 (a i))) → 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_4} [topological_space M] [add_monoid M] [has_continuous_add M] {f : ι → α → M} {x : filter α} {a : ι → M} (l : list ι) :
(∀ (i : ι), i ∈ l → filter.tendsto (f i) x (𝓝 (a i))) → 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} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [monoid M] [has_continuous_mul M] {f : ι → X → M} (l : list ι) (h : ∀ (i : ι), i ∈ l → continuous (f i)) :
continuous (λ (a : X), (list.map (λ (i : ι), f i a) l).prod)
source
theorem continuous_list_sum {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_monoid M] [has_continuous_add M] {f : ι → X → M} (l : list ι) (h : ∀ (i : ι), i ∈ l → continuous (f i)) :
continuous (λ (a : X), (list.map (λ (i : ι), f i a) l).sum)
source
theorem continuous_pow {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (n : ℕ) :
continuous (λ (a : M), a ^ n)
source
theorem continuous.pow {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [monoid M] [has_continuous_mul M] {f : X → M} (h : continuous f) (n : ℕ) :
continuous (λ (b : X), f b ^ n)
source
theorem continuous_on_pow {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {s : set M} (n : ℕ) :
continuous_on (λ (x : M), x ^ n) s
source
theorem continuous_at_pow {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (x : M) (n : ℕ) :
continuous_at (λ (x : M), x ^ n) x
source
theorem filter.tendsto.pow {α : Type u_2} {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {l : filter α} {f : α → M} {x : M} (hf : filter.tendsto f l (𝓝 x)) (n : ℕ) :
filter.tendsto (λ (x : α), f x ^ n) l (𝓝 (x ^ n))
source
theorem continuous_within_at.pow {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [monoid M] [has_continuous_mul M] {f : X → M} {x : X} {s : set X} (hf : continuous_within_at f s x) (n : ℕ) :
continuous_within_at (λ (x : X), f x ^ n) s x
source
theorem continuous_at.pow {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [monoid M] [has_continuous_mul M] {f : X → M} {x : X} (hf : continuous_at f x) (n : ℕ) :
continuous_at (λ (x : X), f x ^ n) x
source
theorem continuous_on.pow {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [monoid M] [has_continuous_mul M] {f : X → M} {s : set X} (hf : continuous_on f s) (n : ℕ) :
continuous_on (λ (x : X), f x ^ n) s
source
@[instance]
def opposite.topological_space {α : Type u_2} [topological_space α] :
topological_space αᵒᵖ

Put the same topological space structure on the opposite monoid as on the original space.

Equations
source
theorem continuous_unop {α : Type u_2} [topological_space α] :
continuous opposite.unop
source
theorem continuous_op {α : Type u_2} [topological_space α] :
continuous opposite.op
source
@[instance]
def opposite.has_continuous_mul {α : Type u_2} [topological_space α] [monoid α] [has_continuous_mul α] :
has_continuous_mul αᵒᵖ

If multiplication is continuous in the monoid α, then it also is in the monoid αᵒᵖ.

source
@[instance]
def units.topological_space {α : Type u_2} [topological_space α] [monoid α] :
topological_space (units α)

The units of a monoid are equipped with a topology, via the embedding into α × α.

Equations
source
theorem units.continuous_embed_product {α : Type u_2} [topological_space α] [monoid α] :
continuous ⇑(embed_product α)
source
theorem units.continuous_coe {α : Type u_2} [topological_space α] [monoid α] :
continuous coe
source
@[instance]
def units.has_continuous_mul {α : Type u_2} [topological_space α] [monoid α] [has_continuous_mul α] :
has_continuous_mul (units α)

If multiplication on a monoid is continuous, then multiplication on the units of the monoid, with respect to the induced topology, is continuous.

Inversion is also continuous, but we register this in a later file, topology.algebra.group, because the predicate has_continuous_inv has not yet been defined.

source
theorem add_submonoid.mem_nhds_zero {M : Type u_4} [topological_space M] [add_comm_monoid M] (S : add_submonoid M) (oS : is_open ↑S) :
↑S ∈ 𝓝 0
source
theorem submonoid.mem_nhds_one {M : Type u_4} [topological_space M] [comm_monoid M] (S : submonoid M) (oS : is_open ↑S) :
↑S ∈ 𝓝 1
source
theorem tendsto_multiset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_4} [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → α → M} {x : filter α} {a : ι → M} (s : multiset ι) :
(∀ (i : ι), i ∈ s → filter.tendsto (f i) x (𝓝 (a i))) → 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_4} [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → α → M} {x : filter α} {a : ι → M} (s : multiset ι) :
(∀ (i : ι), i ∈ s → filter.tendsto (f i) x (𝓝 (a i))) → 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_4} [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → α → M} {x : filter α} {a : ι → M} (s : finset ι) :
(∀ (i : ι), i ∈ s → filter.tendsto (f i) x (𝓝 (a i))) → 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_4} [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → α → M} {x : filter α} {a : ι → M} (s : finset ι) :
(∀ (i : ι), i ∈ s → filter.tendsto (f i) x (𝓝 (a i))) → filter.tendsto (λ (b : α), ∏ (c : ι) in s, f c b) x (𝓝 (∏ (c : ι) in s, a c))
source
theorem continuous_multiset_prod {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → X → M} (s : multiset ι) :
(∀ (i : ι), i ∈ s → continuous (f i)) → continuous (λ (a : X), (multiset.map (λ (i : ι), f i a) s).prod)
source
theorem continuous_multiset_sum {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → X → M} (s : multiset ι) :
(∀ (i : ι), i ∈ s → continuous (f i)) → continuous (λ (a : X), (multiset.map (λ (i : ι), f i a) s).sum)
source
theorem continuous_finset_prod {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → X → M} (s : finset ι) :
(∀ (i : ι), i ∈ s → continuous (f i)) → continuous (λ (a : X), ∏ (i : ι) in s, f i a)
source
theorem continuous_finset_sum {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → X → M} (s : finset ι) :
(∀ (i : ι), i ∈ s → continuous (f i)) → continuous (λ (a : X), ∑ (i : ι) in s, f i a)
source
theorem continuous_finprod {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → X → M} (hc : ∀ (i : ι), continuous (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
continuous (λ (x : X), ∏ᶠ (i : ι), f i x)
source
theorem continuous_finsum {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → X → M} (hc : ∀ (i : ι), continuous (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
continuous (λ (x : X), ∑ᶠ (i : ι), f i x)
source
theorem continuous_finprod_cond {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → X → M} {p : ι → Prop} (hc : ∀ (i : ι), p i → continuous (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
continuous (λ (x : X), ∏ᶠ (i : ι) (hi : p i), f i x)
source
theorem continuous_finsum_cond {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → X → M} {p : ι → Prop} (hc : ∀ (i : ι), p i → continuous (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
continuous (λ (x : X), ∑ᶠ (i : ι) (hi : p i), f i x)
source
@[instance]
def additive.has_continuous_add {M : Type u_1} [h : topological_space M] [has_mul M] [has_continuous_mul M] :
has_continuous_add (additive M)
source
@[instance]
def multiplicative.has_continuous_mul {M : Type u_1} [h : topological_space M] [has_add M] [has_continuous_add M] :
has_continuous_mul (multiplicative M)