@[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_add
{α : Type u_1}
[topological_space α]
[has_add α]
[has_continuous_add α] :
continuous (λ (p : α × α), p.fst + p.snd)
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}
{β : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α]
[topological_space β]
{f g : β → α} :
continuous f → 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 : β → α} :
continuous f → continuous g → continuous (λ (x : β), f x * g x)
theorem
continuous_mul_left
{α : Type u_1}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
(a : α) :
continuous (λ (b : α), a * b)
theorem
continuous_add_left
{α : Type u_1}
[topological_space α]
[has_add α]
[has_continuous_add α]
(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 β} :
continuous_on f s → 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 β} :
continuous_on f s → continuous_on g s → continuous_on (λ (x : β), f x * g x) s
theorem
tendsto_mul
{α : Type u_1}
[topological_space α]
[has_mul α]
[has_continuous_mul α]
{a b : α} :
theorem
tendsto_add
{α : Type u_1}
[topological_space α]
[has_add α]
[has_continuous_add α]
{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 : α} :
filter.tendsto f x (nhds a) → filter.tendsto g x (nhds b) → filter.tendsto (λ (x : β), f x * g x) x (nhds (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 : α} :
filter.tendsto f x (nhds a) → filter.tendsto g x (nhds b) → filter.tendsto (λ (x : β), f x + g x) x (nhds (a + b))
theorem
continuous_at.add
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[has_add α]
[has_continuous_add α]
[topological_space β]
{f g : β → α}
{x : β} :
continuous_at f x → 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 : β} :
continuous_at f x → 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 : β} :
continuous_within_at f s x → 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 : β} :
continuous_within_at f s x → 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 (α × β)
Equations
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 γ) :
(∀ (c : γ), c ∈ l → filter.tendsto (f c) x (nhds (a c))) → filter.tendsto (λ (b : β), (list.map (λ (c : γ), f c b) l).prod) x (nhds (list.map a l).prod)
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 γ) :
(∀ (c : γ), c ∈ l → filter.tendsto (f c) x (nhds (a c))) → filter.tendsto (λ (b : β), (list.map (λ (c : γ), f c b) l).sum) x (nhds (list.map a l).sum)
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 γ) :
(∀ (c : γ), c ∈ l → continuous (f c)) → continuous (λ (a : β), (list.map (λ (c : γ), f c a) l).sum)
theorem
continuous_list_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[monoid α]
[has_continuous_mul α]
[topological_space β]
{f : γ → β → α}
(l : list γ) :
(∀ (c : γ), c ∈ l → continuous (f c)) → continuous (λ (a : β), (list.map (λ (c : γ), f c a) l).prod)
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 α) :
theorem
submonoid.mem_nhds_one
{α : Type u_1}
[topological_space α]
[comm_monoid α]
(β : submonoid α) :
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 γ) :
(∀ (c : γ), c ∈ s → filter.tendsto (f c) x (nhds (a c))) → filter.tendsto (λ (b : β), (multiset.map (λ (c : γ), f c b) s).sum) x (nhds (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 γ) :
(∀ (c : γ), c ∈ s → filter.tendsto (f c) x (nhds (a c))) → filter.tendsto (λ (b : β), (multiset.map (λ (c : γ), f c b) s).prod) x (nhds (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 γ) :
(∀ (c : γ), c ∈ s → filter.tendsto (f c) x (nhds (a c))) → filter.tendsto (λ (b : β), s.sum (λ (c : γ), f c b)) x (nhds (s.sum (λ (c : γ), 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 γ) :
(∀ (c : γ), c ∈ s → filter.tendsto (f c) x (nhds (a c))) → filter.tendsto (λ (b : β), s.prod (λ (c : γ), f c b)) x (nhds (s.prod (λ (c : γ), 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 γ) :
(∀ (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 γ) :
(∀ (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 γ) :
(∀ (c : γ), c ∈ s → continuous (f c)) → continuous (λ (a : β), s.prod (λ (c : γ), 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 γ) :
(∀ (c : γ), c ∈ s → continuous (f c)) → continuous (λ (a : β), s.sum (λ (c : γ), f c a))