@[class]
- continuous_add : continuous (λ (p : α × α), 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 α.
@[class]
- continuous_mul : continuous (λ (p : α × α), (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
{α : Type u_1}
[topological_space α]
[has_mul α]
[has_continuous_mul α] :
continuous (λ (p : α × α), (p.fst) * p.snd)
theorem
continuous_add
{α : Type u_1}
[topological_space α]
[has_add α]
[has_continuous_add α] :
continuous (λ (p : α × α), p.fst + p.snd)
theorem
continuous.add
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α]
[topological_space β]
{f g : β → α}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : β), f x + g x)
theorem
continuous.mul
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
[topological_space β]
{f g : β → α}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : β), (f x) * g x)
theorem
continuous_add_left
{α : Type u_1}
[topological_space α]
[has_add α]
[has_continuous_add α]
(a : α) :
continuous (λ (b : α), a + b)
theorem
continuous_mul_left
{α : Type u_1}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
(a : α) :
continuous (λ (b : α), a * b)
theorem
continuous_add_right
{α : Type u_1}
[topological_space α]
[has_add α]
[has_continuous_add α]
(a : α) :
continuous (λ (b : α), b + a)
theorem
continuous_mul_right
{α : Type u_1}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
(a : α) :
continuous (λ (b : α), b * a)
theorem
continuous_on.add
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α]
[topological_space β]
{f g : β → α}
{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}
{β : Type u_2}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
[topological_space β]
{f g : β → α}
{s : set β}
(hf : continuous_on f s)
(hg : continuous_on g s) :
continuous_on (λ (x : β), (f x) * g x) s
theorem
tendsto_add
{α : Type u_1}
[topological_space α]
[has_add α]
[has_continuous_add α]
{a b : α} :
theorem
tendsto_mul
{α : Type u_1}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
{a b : α} :
theorem
filter.tendsto.add
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α]
{f g : β → α}
{x : filter β}
{a b : α}
(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}
{β : Type u_2}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
{f g : β → α}
{x : filter β}
{a b : α}
(hf : filter.tendsto f x (𝓝 a))
(hg : filter.tendsto g x (𝓝 b)) :
filter.tendsto (λ (x : β), (f x) * g x) x (𝓝 (a * b))
theorem
continuous_at.add
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α]
[topological_space β]
{f g : β → α}
{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}
{β : Type u_2}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
[topological_space β]
{f g : β → α}
{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}
{β : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α]
[topological_space β]
{f g : β → α}
{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}
{β : Type u_2}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
[topological_space β]
{f g : β → α}
{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
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α]
[topological_space β]
[has_add β]
[has_continuous_add β] :
has_continuous_add (α × β)
@[instance]
def
prod.has_continuous_mul
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
[topological_space β]
[has_mul β]
[has_continuous_mul β] :
has_continuous_mul (α × β)
theorem
tendsto_list_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[monoid α]
[has_continuous_mul α]
{f : γ → β → α}
{x : filter β}
{a : γ → α}
(l : list γ)
(a_1 : ∀ (c : γ), c ∈ l → filter.tendsto (f c) x (𝓝 (a c))) :
theorem
tendsto_list_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[add_monoid α]
[has_continuous_add α]
{f : γ → β → α}
{x : filter β}
{a : γ → α}
(l : list γ)
(a_1 : ∀ (c : γ), c ∈ l → filter.tendsto (f c) x (𝓝 (a c))) :
theorem
continuous_list_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[monoid α]
[has_continuous_mul α]
[topological_space β]
{f : γ → β → α}
(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}
{γ : Type u_3}
[topological_space α]
[add_monoid α]
[has_continuous_add α]
[topological_space β]
{f : γ → β → α}
(l : list γ)
(h : ∀ (c : γ), c ∈ l → continuous (f c)) :
continuous (λ (a : β), (list.map (λ (c : γ), f c a) l).sum)
theorem
continuous_pow
{α : Type u_1}
[topological_space α]
[monoid α]
[has_continuous_mul α]
(n : ℕ) :
continuous (λ (a : α), a ^ n)
theorem
continuous.pow
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[monoid α]
[has_continuous_mul α]
{f : β → α}
[topological_space β]
(h : continuous f)
(n : ℕ) :
continuous (λ (b : β), f b ^ n)
theorem
add_submonoid.mem_nhds_zero
{α : Type u_1}
[topological_space α]
[add_comm_monoid α]
(β : add_submonoid α)
(oβ : is_open ↑β) :
theorem
submonoid.mem_nhds_one
{α : Type u_1}
[topological_space α]
[comm_monoid α]
(β : submonoid α)
(oβ : is_open ↑β) :
theorem
tendsto_multiset_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[add_comm_monoid α]
[has_continuous_add α]
{f : γ → β → α}
{x : filter β}
{a : γ → α}
(s : multiset γ)
(a_1 : ∀ (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}
{γ : Type u_3}
[topological_space α]
[comm_monoid α]
[has_continuous_mul α]
{f : γ → β → α}
{x : filter β}
{a : γ → α}
(s : multiset γ)
(a_1 : ∀ (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}
{γ : Type u_3}
[topological_space α]
[add_comm_monoid α]
[has_continuous_add α]
{f : γ → β → α}
{x : filter β}
{a : γ → α}
(s : finset γ)
(a_1 : ∀ (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}
{γ : Type u_3}
[topological_space α]
[comm_monoid α]
[has_continuous_mul α]
{f : γ → β → α}
{x : filter β}
{a : γ → α}
(s : finset γ)
(a_1 : ∀ (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}
{γ : Type u_3}
[topological_space α]
[comm_monoid α]
[has_continuous_mul α]
[topological_space β]
{f : γ → β → α}
(s : multiset γ)
(a : ∀ (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}
{γ : Type u_3}
[topological_space α]
[add_comm_monoid α]
[has_continuous_add α]
[topological_space β]
{f : γ → β → α}
(s : multiset γ)
(a : ∀ (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}
{γ : Type u_3}
[topological_space α]
[comm_monoid α]
[has_continuous_mul α]
[topological_space β]
{f : γ → β → α}
(s : finset γ)
(a : ∀ (c : γ), c ∈ s → continuous (f c)) :
continuous (λ (a : β), ∏ (c : γ) in s, f c a)
theorem
continuous_finset_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[add_comm_monoid α]
[has_continuous_add α]
[topological_space β]
{f : γ → β → α}
(s : finset γ)
(a : ∀ (c : γ), c ∈ s → continuous (f c)) :
continuous (λ (a : β), ∑ (c : γ) in s, f c a)