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_semiring.to_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
- add_opposite.has_continuous_add
- add_units.has_continuous_add
- additive.has_continuous_add
- mul_opposite.has_continuous_add
- order_dual.has_continuous_add
- number_field.pi.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
- topological_semiring.to_has_continuous_mul
- linear_ordered_field.has_continuous_mul
- 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
- add_opposite.has_continuous_mul
- order_dual.has_continuous_mul
- topological_ring.top_monoid_units
- finite_adele_ring'.has_continuous_mul
- number_field.pi.has_continuous_mul
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)
@[protected, instance]
def
has_continuous_add.has_continuous_vadd
{M : Type u_4}
[topological_space M]
[has_add M]
[has_continuous_add M] :
@[protected, instance]
def
has_continuous_mul.has_continuous_smul
{M : Type u_4}
[topological_space M]
[has_mul M]
[has_continuous_mul M] :
@[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))
@[simp]
theorem
filter.tendsto.coe_inv_units
{ι : Type u_1}
{N : Type u_5}
[topological_space N]
[monoid N]
[has_continuous_mul N]
[t2_space N]
{f : ι → Nˣ}
{r₁ r₂ : N}
{l : filter ι}
[l.ne_bot]
(h₁ : filter.tendsto (λ (x : ι), ↑(f x)) l (𝓝 r₁))
(h₂ : filter.tendsto (λ (x : ι), ↑(f x)⁻¹) l (𝓝 r₂)) :
def
filter.tendsto.add_units
{ι : Type u_1}
{N : Type u_5}
[topological_space N]
[add_monoid N]
[has_continuous_add N]
[t2_space N]
{f : ι → add_units N}
{r₁ r₂ : N}
{l : filter ι}
[l.ne_bot]
(h₁ : filter.tendsto (λ (x : ι), ↑(f x)) l (𝓝 r₁))
(h₂ : filter.tendsto (λ (x : ι), ↑-f x) l (𝓝 r₂)) :
Construct an additive unit from limits of additive units and their negatives.
@[simp]
theorem
filter.tendsto.coe_add_units
{ι : Type u_1}
{N : Type u_5}
[topological_space N]
[add_monoid N]
[has_continuous_add N]
[t2_space N]
{f : ι → add_units N}
{r₁ r₂ : N}
{l : filter ι}
[l.ne_bot]
(h₁ : filter.tendsto (λ (x : ι), ↑(f x)) l (𝓝 r₁))
(h₂ : filter.tendsto (λ (x : ι), ↑-f x) l (𝓝 r₂)) :
@[simp]
theorem
filter.tendsto.coe_neg_add_units
{ι : Type u_1}
{N : Type u_5}
[topological_space N]
[add_monoid N]
[has_continuous_add N]
[t2_space N]
{f : ι → add_units N}
{r₁ r₂ : N}
{l : filter ι}
[l.ne_bot]
(h₁ : filter.tendsto (λ (x : ι), ↑(f x)) l (𝓝 r₁))
(h₂ : filter.tendsto (λ (x : ι), ↑-f x) l (𝓝 r₂)) :
def
filter.tendsto.units
{ι : Type u_1}
{N : Type u_5}
[topological_space N]
[monoid N]
[has_continuous_mul N]
[t2_space N]
{f : ι → Nˣ}
{r₁ r₂ : N}
{l : filter ι}
[l.ne_bot]
(h₁ : filter.tendsto (λ (x : ι), ↑(f x)) l (𝓝 r₁))
(h₂ : filter.tendsto (λ (x : ι), ↑(f x)⁻¹) l (𝓝 r₂)) :
Nˣ
Construct a unit from limits of units and their inverses.
@[simp]
theorem
filter.tendsto.coe_units
{ι : Type u_1}
{N : Type u_5}
[topological_space N]
[monoid N]
[has_continuous_mul N]
[t2_space N]
{f : ι → Nˣ}
{r₁ r₂ : N}
{l : filter ι}
[l.ne_bot]
(h₁ : filter.tendsto (λ (x : ι), ↑(f x)) l (𝓝 r₁))
(h₂ : filter.tendsto (λ (x : ι), ↑(f x)⁻¹) l (𝓝 r₂)) :
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
def
submonoid.comm_monoid_topological_closure
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
[t2_space M]
(s : submonoid M)
(hs : ∀ (x y : ↥s), x * y = y * x) :
If a submonoid of a topological monoid is commutative, then so is its topological closure.
Equations
- s.comm_monoid_topological_closure hs = {mul := monoid.mul s.topological_closure.to_monoid, mul_assoc := _, one := monoid.one s.topological_closure.to_monoid, one_mul := _, mul_one := _, npow := monoid.npow s.topological_closure.to_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
def
add_submonoid.add_comm_monoid_topological_closure
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
[t2_space M]
(s : add_submonoid M)
(hs : ∀ (x y : ↥s), x + y = y + x) :
If a submonoid of an additive topological monoid is commutative, then so is its topological closure.
Equations
- s.add_comm_monoid_topological_closure hs = {add := add_monoid.add s.topological_closure.to_add_monoid, add_assoc := _, zero := add_monoid.zero s.topological_closure.to_add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul s.topological_closure.to_add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
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
is_compact.add
{M : Type u_4}
[topological_space M]
[add_monoid M]
[has_continuous_add M]
{s t : set M}
(hs : is_compact s)
(ht : is_compact t) :
is_compact (s + t)
theorem
is_compact.mul
{M : Type u_4}
[topological_space M]
[monoid M]
[has_continuous_mul M]
{s t : set M}
(hs : is_compact s)
(ht : is_compact t) :
is_compact (s * t)
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)
@[protected, instance]
def
add_monoid.has_continuous_const_smul_nat
{A : Type u_1}
[add_monoid A]
[topological_space A]
[has_continuous_add A] :
@[protected, instance]
def
add_monoid.has_continuous_smul_nat
{A : Type u_1}
[add_monoid A]
[topological_space A]
[has_continuous_add 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]
def
mul_opposite.has_continuous_mul
{α : Type u_2}
[topological_space α]
[has_mul α]
[has_continuous_mul α] :
If multiplication is continuous in α, then it also is in αᵐᵒᵖ.
@[protected, instance]
def
add_opposite.has_continuous_add
{α : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α] :
If addition is continuous in α, then it also is in αᵃᵒᵖ.
@[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.
@[protected, instance]
def
add_units.has_continuous_add
{α : Type u_2}
[topological_space α]
[add_monoid α]
[has_continuous_add α] :
If addition on an additive monoid is continuous, then addition on the additive units of the monoid, with respect to the induced topology, is continuous.
Negation is also continuous, but we register this in a later file, topology.algebra.group, because
the predicate has_continuous_neg 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
locally_finite.exists_finset_mul_support
{ι : Type u_1}
{X : Type u_3}
[topological_space X]
{M : Type u_2}
[comm_monoid M]
{f : ι → X → M}
(hf : locally_finite (λ (i : ι), function.mul_support (f i)))
(x₀ : X) :
∃ (I : finset ι), ∀ᶠ (x : X) in 𝓝 x₀, function.mul_support (λ (i : ι), f i x) ⊆ ↑I
theorem
locally_finite.exists_finset_support
{ι : Type u_1}
{X : Type u_3}
[topological_space X]
{M : Type u_2}
[add_comm_monoid M]
{f : ι → X → M}
(hf : locally_finite (λ (i : ι), function.support (f i)))
(x₀ : X) :
∃ (I : finset ι), ∀ᶠ (x : X) in 𝓝 x₀, function.support (λ (i : ι), f i x) ⊆ ↑I
theorem
finsum_eventually_eq_sum
{ι : Type u_1}
{X : Type u_3}
[topological_space X]
{M : Type u_2}
[add_comm_monoid M]
{f : ι → X → M}
(hf : locally_finite (λ (i : ι), function.support (f i)))
(x : X) :
theorem
finprod_eventually_eq_prod
{ι : Type u_1}
{X : Type u_3}
[topological_space X]
{M : Type u_2}
[comm_monoid M]
{f : ι → X → M}
(hf : locally_finite (λ (i : ι), function.mul_support (f i)))
(x : X) :
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] :
theorem
has_continuous_mul_Inf
{M : Type u_4}
[has_mul M]
{ts : set (topological_space M)}
(h : ∀ (t : topological_space M), t ∈ ts → has_continuous_mul M) :
theorem
has_continuous_add_Inf
{M : Type u_4}
[has_add M]
{ts : set (topological_space M)}
(h : ∀ (t : topological_space M), t ∈ ts → has_continuous_add M) :
theorem
has_continuous_mul_infi
{M : Type u_4}
{ι' : Sort u_6}
[has_mul M]
{ts' : ι' → topological_space M}
(h' : ∀ (i : ι'), has_continuous_mul M) :
theorem
has_continuous_add_infi
{M : Type u_4}
{ι' : Sort u_6}
[has_add M]
{ts' : ι' → topological_space M}
(h' : ∀ (i : ι'), has_continuous_add M) :
theorem
has_continuous_mul_inf
{M : Type u_4}
[has_mul M]
{t₁ t₂ : topological_space M}
(h₁ : has_continuous_mul M)
(h₂ : has_continuous_mul M) :
theorem
has_continuous_add_inf
{M : Type u_4}
[has_add M]
{t₁ t₂ : topological_space M}
(h₁ : has_continuous_add M)
(h₂ : has_continuous_add M) :
theorem
has_continuous_mul_induced
{M : Type u_4}
{N : Type u_5}
[has_mul M]
[has_mul N]
{t : topological_space N}
[has_continuous_mul N]
{F : Type u_7}
[mul_hom_class F M N]
(f : F) :
theorem
has_continuous_add_induced
{M : Type u_4}
{N : Type u_5}
[has_add M]
[has_add N]
{t : topological_space N}
[has_continuous_add N]
{F : Type u_7}
[add_hom_class F M N]
(f : F) :