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.
theorem
continuous_zero
{X : Type u_3}
{M : Type u_4}
[topological_space X]
[topological_space M]
[has_zero M] :
theorem
continuous_one
{X : Type u_3}
{M : Type u_4}
[topological_space X]
[topological_space M]
[has_one M] :
@[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 M, for example, is obtained by requiring both the
instances add_monoid M and has_continuous_add M.
Instances
- has_continuous_add_of_discrete_topology
- topological_add_group.to_has_continuous_add
- topological_ring.to_has_continuous_add
- has_lipschitz_add.has_continuous_add
- prod.has_continuous_add
- pi.has_continuous_add
- pi.has_continuous_add'
- add_submonoid.has_continuous_add
- add_submonoid.topological_closure_has_continuous_add
- additive.has_continuous_add
- order_dual.has_continuous_add
- ennreal.has_continuous_add
- weak_dual.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 M, for example, is obtained by requiring both the instances monoid M
and has_continuous_mul M.
Instances
- has_continuous_mul_of_discrete_topology
- topological_group.to_has_continuous_mul
- linear_ordered_field.has_continuous_mul
- topological_ring.to_has_continuous_mul
- has_lipschitz_mul.has_continuous_mul
- semi_normed_ring_top_monoid
- linear_ordered_comm_group_with_zero.has_continuous_mul
- prod.has_continuous_mul
- pi.has_continuous_mul
- pi.has_continuous_mul'
- submonoid.has_continuous_mul
- submonoid.topological_closure_has_continuous_mul
- mul_opposite.has_continuous_mul
- units.has_continuous_mul
- multiplicative.has_continuous_mul
- order_dual.has_continuous_mul
- topological_ring.top_monoid_units
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)
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)
@[continuity]
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)
@[continuity]
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)
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)
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)
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)
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)
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
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
theorem
tendsto_add
{M : Type u_4}
[topological_space M]
[has_add M]
[has_continuous_add M]
{a b : M} :
theorem
tendsto_mul
{M : Type u_4}
[topological_space M]
[has_mul M]
[has_continuous_mul M]
{a b : M} :
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))
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))
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))
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))
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))
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))
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
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
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
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
@[protected, 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)
@[protected, 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)
@[protected, 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)
@[protected, 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)
@[protected, 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.
@[protected, 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.
@[protected, instance]
def
has_continuous_mul_of_discrete_topology
{N : Type u_5}
[topological_space N]
[has_mul N]
[discrete_topology N] :
@[protected, instance]
def
has_continuous_add_of_discrete_topology
{N : Type u_5}
[topological_space N]
[has_add N]
[discrete_topology N] :
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)) :
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)) :
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)) :
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)) :
theorem
is_closed_set_of_map_zero
(M₁ : Type u_6)
(M₂ : Type u_7)
[topological_space M₂]
[t2_space M₂]
[has_zero M₁]
[has_zero M₂] :
theorem
is_closed_set_of_map_one
(M₁ : Type u_6)
(M₂ : Type u_7)
[topological_space M₂]
[t2_space M₂]
[has_one M₁]
[has_one M₂] :
theorem
is_closed_set_of_map_add
(M₁ : Type u_6)
(M₂ : Type u_7)
[topological_space M₂]
[t2_space M₂]
[has_add M₁]
[has_add M₂]
[has_continuous_add M₂] :
theorem
is_closed_set_of_map_mul
(M₁ : Type u_6)
(M₂ : Type u_7)
[topological_space M₂]
[t2_space M₂]
[has_mul M₁]
[has_mul M₂]
[has_continuous_mul M₂] :
def
monoid_hom_of_mem_closure_range_coe
{M₁ : Type u_6}
{M₂ : Type u_7}
[topological_space M₂]
[t2_space M₂]
[mul_one_class M₁]
[mul_one_class M₂]
[has_continuous_mul M₂]
{F : Type u_8}
[monoid_hom_class F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (set.range (λ (f : F) (x : M₁), ⇑f x))) :
M₁ →* M₂
Construct a bundled monoid homomorphism M₁ →* M₂ from a function f and a proof that it
belongs to the closure of the range of the coercion from M₁ →* M₂ (or another type of bundled
homomorphisms that has a monoid_hom_class instance) to M₁ → M₂.
@[simp]
theorem
monoid_hom_of_mem_closure_range_coe_apply
{M₁ : Type u_6}
{M₂ : Type u_7}
[topological_space M₂]
[t2_space M₂]
[mul_one_class M₁]
[mul_one_class M₂]
[has_continuous_mul M₂]
{F : Type u_8}
[monoid_hom_class F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (set.range (λ (f : F) (x : M₁), ⇑f x))) :
⇑(monoid_hom_of_mem_closure_range_coe f hf) = f
def
add_monoid_hom_of_mem_closure_range_coe
{M₁ : Type u_6}
{M₂ : Type u_7}
[topological_space M₂]
[t2_space M₂]
[add_zero_class M₁]
[add_zero_class M₂]
[has_continuous_add M₂]
{F : Type u_8}
[add_monoid_hom_class F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (set.range (λ (f : F) (x : M₁), ⇑f x))) :
M₁ →+ M₂
Construct a bundled additive monoid homomorphism M₁ →+ M₂ from a function f
and a proof that it belongs to the closure of the range of the coercion from M₁ →+ M₂ (or another
type of bundled homomorphisms that has a add_monoid_hom_class instance) to M₁ → M₂.
@[simp]
theorem
add_monoid_hom_of_mem_closure_range_coe_apply
{M₁ : Type u_6}
{M₂ : Type u_7}
[topological_space M₂]
[t2_space M₂]
[add_zero_class M₁]
[add_zero_class M₂]
[has_continuous_add M₂]
{F : Type u_8}
[add_monoid_hom_class F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (set.range (λ (f : F) (x : M₁), ⇑f x))) :
@[simp]
theorem
add_monoid_hom_of_tendsto_apply
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[topological_space M₂]
[t2_space M₂]
[add_zero_class M₁]
[add_zero_class M₂]
[has_continuous_add M₂]
{F : Type u_8}
[add_monoid_hom_class F M₁ M₂]
{l : filter α}
(f : M₁ → M₂)
(g : α → F)
[l.ne_bot]
(h : filter.tendsto (λ (a : α) (x : M₁), ⇑(g a) x) l (𝓝 f)) :
⇑(add_monoid_hom_of_tendsto f g h) = f
@[simp]
theorem
monoid_hom_of_tendsto_apply
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[topological_space M₂]
[t2_space M₂]
[mul_one_class M₁]
[mul_one_class M₂]
[has_continuous_mul M₂]
{F : Type u_8}
[monoid_hom_class F M₁ M₂]
{l : filter α}
(f : M₁ → M₂)
(g : α → F)
[l.ne_bot]
(h : filter.tendsto (λ (a : α) (x : M₁), ⇑(g a) x) l (𝓝 f)) :
⇑(monoid_hom_of_tendsto f g h) = f
def
monoid_hom_of_tendsto
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[topological_space M₂]
[t2_space M₂]
[mul_one_class M₁]
[mul_one_class M₂]
[has_continuous_mul M₂]
{F : Type u_8}
[monoid_hom_class F M₁ M₂]
{l : filter α}
(f : M₁ → M₂)
(g : α → F)
[l.ne_bot]
(h : filter.tendsto (λ (a : α) (x : M₁), ⇑(g a) x) l (𝓝 f)) :
M₁ →* M₂
Construct a bundled monoid homomorphism from a pointwise limit of monoid homomorphisms.
Equations
def
add_monoid_hom_of_tendsto
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[topological_space M₂]
[t2_space M₂]
[add_zero_class M₁]
[add_zero_class M₂]
[has_continuous_add M₂]
{F : Type u_8}
[add_monoid_hom_class F M₁ M₂]
{l : filter α}
(f : M₁ → M₂)
(g : α → F)
[l.ne_bot]
(h : filter.tendsto (λ (a : α) (x : M₁), ⇑(g a) x) l (𝓝 f)) :
M₁ →+ M₂
Construct a bundled additive monoid homomorphism from a pointwise limit of additive monoid homomorphisms
Equations
theorem
add_monoid_hom.is_closed_range_coe
(M₁ : Type u_6)
(M₂ : Type u_7)
[topological_space M₂]
[t2_space M₂]
[add_zero_class M₁]
[add_zero_class M₂]
[has_continuous_add M₂] :
theorem
monoid_hom.is_closed_range_coe
(M₁ : Type u_6)
(M₂ : Type u_7)
[topological_space M₂]
[t2_space M₂]
[mul_one_class M₁]
[mul_one_class M₂]
[has_continuous_mul M₂] :
@[protected, instance]
def
submonoid.has_continuous_mul
{α : Type u_2}
[topological_space α]
[monoid α]
[has_continuous_mul α]
(S : submonoid α) :
@[protected, instance]
def
add_submonoid.has_continuous_add
{α : Type u_2}
[topological_space α]
[add_monoid α]
[has_continuous_add α]
(S : add_submonoid α) :
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) :
theorem
submonoid.top_closure_mul_self_subset
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
(s : submonoid M) :
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) :
theorem
submonoid.top_closure_mul_self_eq
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
(s : submonoid M) :
def
submonoid.topological_closure
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
(s : submonoid M) :
The (topological-space) closure of a submonoid of a space M with has_continuous_mul is
itself a submonoid.
def
add_submonoid.topological_closure
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
(s : add_submonoid M) :
The (topological-space) closure of an additive submonoid of a space M with
has_continuous_add is itself an additive submonoid.
@[protected, instance]
def
submonoid.topological_closure_has_continuous_mul
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
(s : submonoid M) :
@[protected, 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) :
theorem
add_submonoid.add_submonoid_topological_closure
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
(s : add_submonoid M) :
s ≤ s.topological_closure
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
theorem
add_submonoid.is_closed_topological_closure
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
(s : add_submonoid M) :
theorem
submonoid.is_closed_topological_closure
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
(s : submonoid M) :
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
theorem
add_submonoid.topological_closure_minimal
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
(s : add_submonoid M)
{t : add_submonoid M}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
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) :
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) :
theorem
exists_nhds_one_split
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
{s : set M}
(hs : s ∈ 𝓝 1) :
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) :
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) :
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_4}
[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_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)
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)
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)
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)
@[continuity]
theorem
continuous_pow
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
(n : ℕ) :
continuous (λ (a : M), a ^ n)
@[continuity]
theorem
continuous_nsmul
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
(n : ℕ) :
continuous (λ (a : M), n • a)
@[continuity]
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)
@[continuity]
theorem
continuous.nsmul
{X : Type u_3}
{M : Type u_4}
[topological_space X]
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{f : X → M}
(h : continuous f)
(n : ℕ) :
continuous (λ (b : X), n • f b)
theorem
continuous_on_nsmul
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{s : set M}
(n : ℕ) :
continuous_on (λ (x : M), n • x) s
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
theorem
continuous_at_nsmul
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
(x : M)
(n : ℕ) :
continuous_at (λ (x : M), n • x) x
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
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))
theorem
filter.tendsto.nsmul
{α : Type u_2}
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{l : filter α}
{f : α → M}
{x : M}
(hf : filter.tendsto f l (𝓝 x))
(n : ℕ) :
filter.tendsto (λ (x : α), n • f x) l (𝓝 (n • x))
theorem
continuous_within_at.nsmul
{X : Type u_3}
{M : Type u_4}
[topological_space X]
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{f : X → M}
{x : X}
{s : set X}
(hf : continuous_within_at f s x)
(n : ℕ) :
continuous_within_at (λ (x : X), n • f x) s x
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
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
theorem
continuous_at.nsmul
{X : Type u_3}
{M : Type u_4}
[topological_space X]
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{f : X → M}
{x : X}
(hf : continuous_at f x)
(n : ℕ) :
continuous_at (λ (x : X), n • f x) x
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
theorem
continuous_on.nsmul
{X : Type u_3}
{M : Type u_4}
[topological_space X]
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{f : X → M}
{s : set X}
(hf : continuous_on f s)
(n : ℕ) :
continuous_on (λ (x : X), n • f x) s
@[protected, instance]
Put the same topological space structure on the opposite monoid as on the original space.
@[protected, instance]
def
mul_opposite.has_continuous_mul
{α : Type u_2}
[topological_space α]
[monoid α]
[has_continuous_mul α] :
If multiplication is continuous in the monoid α, then it also is in the monoid αᵐᵒᵖ.
@[protected, instance]
The units of a monoid are equipped with a topology, via the embedding into α × α.
@[protected, instance]
def
units.has_continuous_mul
{α : Type u_2}
[topological_space α]
[monoid α]
[has_continuous_mul α] :
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.
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) :
theorem
submonoid.mem_nhds_one
{M : Type u_4}
[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_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)
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)
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))
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))
@[continuity]
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)
@[continuity]
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)
@[continuity]
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)
@[continuity]
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)
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)
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)
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)
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)
@[protected, instance]
def
additive.has_continuous_add
{M : Type u_1}
[h : topological_space M]
[has_mul M]
[has_continuous_mul M] :
@[protected, instance]
def
multiplicative.has_continuous_mul
{M : Type u_1}
[h : topological_space M]
[has_add M]
[has_continuous_add M] :