topology.algebra.monoid

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

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.

Continuity in only the left/right argument can be stated using has_continuous_const_vadd α α/has_continuous_const_vadd αᵐᵒᵖ α.

Instances of this typeclass

source

@[class]

structure has_continuous_mul (M : Type u) [topological_space M] [has_mul M] :

Prop

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.

Continuity in only the left/right argument can be stated using has_continuous_const_smul α α/has_continuous_const_smul αᵐᵒᵖ α.

Instances of this typeclass

source

@[protected, instance]

def order_dual.has_continuous_add {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] :

has_continuous_add Mᵒᵈ

source

@[protected, instance]

def order_dual.has_continuous_mul {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] :

has_continuous_mul Mᵒᵈ

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

@[protected, instance]

def has_continuous_add.to_has_continuous_vadd {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] :

has_continuous_vadd M M

source

@[protected, instance]

def has_continuous_mul.to_has_continuous_smul {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] :

has_continuous_smul M M

source

@[protected, instance]

def has_continuous_add.to_has_continuous_vadd_op {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] :

has_continuous_vadd Mᵃᵒᵖ M

source

@[protected, instance]

def has_continuous_mul.to_has_continuous_smul_op {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] :

has_continuous_smul Mᵐᵒᵖ M

source

@[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)

source

@[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)

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) (nhds (a, b)) (nhds (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) (nhds (a, b)) (nhds (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 (nhds a)) (hg : filter.tendsto g x (nhds b)) :

filter.tendsto (λ (x : α), f x + g x) x (nhds (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 (nhds a)) (hg : filter.tendsto g x (nhds b)) :

filter.tendsto (λ (x : α), f x * g x) x (nhds (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 (nhds c)) :

filter.tendsto (λ (k : α), b + f k) l (nhds (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 (nhds c)) :

filter.tendsto (λ (k : α), b * f k) l (nhds (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 (nhds c)) :

filter.tendsto (λ (k : α), f k * b) l (nhds (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 (nhds c)) :

filter.tendsto (λ (k : α), f k + b) l (nhds (c + b))

source

theorem le_nhds_mul {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] (a b : M) :

nhds a * nhds b ≤ nhds (a * b)

source

theorem le_nhds_add {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] (a b : M) :

nhds a + nhds b ≤ nhds (a + b)

source

@[simp]

theorem nhds_zero_add_nhds {M : Type u_1} [add_zero_class M] [topological_space M] [has_continuous_add M] (a : M) :

nhds 0 + nhds a = nhds a

source

@[simp]

theorem nhds_one_mul_nhds {M : Type u_1} [mul_one_class M] [topological_space M] [has_continuous_mul M] (a : M) :

nhds 1 * nhds a = nhds a

source

@[simp]

theorem nhds_mul_nhds_one {M : Type u_1} [mul_one_class M] [topological_space M] [has_continuous_mul M] (a : M) :

nhds a * nhds 1 = nhds a

source

@[simp]

theorem nhds_add_nhds_zero {M : Type u_1} [add_zero_class M] [topological_space M] [has_continuous_add M] (a : M) :

nhds a + nhds 0 = nhds a

source

theorem filter.tendsto_nhds_within_Ioi.const_mul {α : Type u_2} {𝕜 : Type u_6} [preorder 𝕜] [has_zero 𝕜] [has_mul 𝕜] [topological_space 𝕜] [has_continuous_mul 𝕜] {l : filter α} {f : α → 𝕜} {b c : 𝕜} (hb : 0 < b) [pos_mul_strict_mono 𝕜] [pos_mul_reflect_lt 𝕜] (h : filter.tendsto f l (nhds_within c (set.Ioi c))) :

filter.tendsto (λ (a : α), b * f a) l (nhds_within (b * c) (set.Ioi (b * c)))

source

theorem filter.tendsto_nhds_within_Iio.const_mul {α : Type u_2} {𝕜 : Type u_6} [preorder 𝕜] [has_zero 𝕜] [has_mul 𝕜] [topological_space 𝕜] [has_continuous_mul 𝕜] {l : filter α} {f : α → 𝕜} {b c : 𝕜} (hb : 0 < b) [pos_mul_strict_mono 𝕜] [pos_mul_reflect_lt 𝕜] (h : filter.tendsto f l (nhds_within c (set.Iio c))) :

filter.tendsto (λ (a : α), b * f a) l (nhds_within (b * c) (set.Iio (b * c)))

source

theorem filter.tendsto_nhds_within_Ioi.mul_const {α : Type u_2} {𝕜 : Type u_6} [preorder 𝕜] [has_zero 𝕜] [has_mul 𝕜] [topological_space 𝕜] [has_continuous_mul 𝕜] {l : filter α} {f : α → 𝕜} {b c : 𝕜} (hb : 0 < b) [mul_pos_strict_mono 𝕜] [mul_pos_reflect_lt 𝕜] (h : filter.tendsto f l (nhds_within c (set.Ioi c))) :

filter.tendsto (λ (a : α), f a * b) l (nhds_within (c * b) (set.Ioi (c * b)))

source

theorem filter.tendsto_nhds_within_Iio.mul_const {α : Type u_2} {𝕜 : Type u_6} [preorder 𝕜] [has_zero 𝕜] [has_mul 𝕜] [topological_space 𝕜] [has_continuous_mul 𝕜] {l : filter α} {f : α → 𝕜} {b c : 𝕜} (hb : 0 < b) [mul_pos_strict_mono 𝕜] [mul_pos_reflect_lt 𝕜] (h : filter.tendsto f l (nhds_within c (set.Iio c))) :

filter.tendsto (λ (a : α), f a * b) l (nhds_within (c * b) (set.Iio (c * b)))

source

@[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 (nhds r₁)) (h₂ : filter.tendsto (λ (x : ι), ↑(f x)⁻¹) l (nhds r₂)) :

↑(h₁.units h₂)⁻¹ = r₂

source

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 (nhds r₁)) (h₂ : filter.tendsto (λ (x : ι), ↑-f x) l (nhds r₂)) :

add_units N

Construct an additive unit from limits of additive units and their negatives.

Equations

h₁.add_units h₂ = {val := r₁, neg := r₂, val_neg := _, neg_val := _}

source

@[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 (nhds r₁)) (h₂ : filter.tendsto (λ (x : ι), ↑-f x) l (nhds r₂)) :

↑(h₁.add_units h₂) = r₁

source

@[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 (nhds r₁)) (h₂ : filter.tendsto (λ (x : ι), ↑-f x) l (nhds r₂)) :

↑-h₁.add_units h₂ = r₂

source

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 (nhds r₁)) (h₂ : filter.tendsto (λ (x : ι), ↑(f x)⁻¹) l (nhds r₂)) :

Nˣ

Construct a unit from limits of units and their inverses.

Equations

h₁.units h₂ = {val := r₁, inv := r₂, val_inv := _, inv_val := _}

source

@[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 (nhds r₁)) (h₂ : filter.tendsto (λ (x : ι), ↑(f x)⁻¹) l (nhds r₂)) :

↑(h₁.units h₂) = r₁

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

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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.

source

@[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.

source

@[protected, 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

@[protected, 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) ((nhds 0).prod (nhds 0)) (nhds 0)) (hleft : ∀ (x₀ : M), nhds x₀ = filter.map (λ (x : M), x₀ + x) (nhds 0)) (hright : ∀ (x₀ : M), nhds x₀ = filter.map (λ (x : M), x + x₀) (nhds 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) ((nhds 1).prod (nhds 1)) (nhds 1)) (hleft : ∀ (x₀ : M), nhds x₀ = filter.map (λ (x : M), x₀ * x) (nhds 1)) (hright : ∀ (x₀ : M), nhds x₀ = filter.map (λ (x : M), x * x₀) (nhds 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) ((nhds 1).prod (nhds 1)) (nhds 1)) (hleft : ∀ (x₀ : M), nhds x₀ = filter.map (λ (x : M), x₀ * x) (nhds 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) ((nhds 0).prod (nhds 0)) (nhds 0)) (hleft : ∀ (x₀ : M), nhds x₀ = filter.map (λ (x : M), x₀ + x) (nhds 0)) :

has_continuous_add M

source

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₂] :

is_closed {f : M₁ → M₂ | f 0 = 0}

source

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₂] :

is_closed {f : M₁ → M₂ | f 1 = 1}

source

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₂] :

is_closed {f : M₁ → M₂ | ∀ (x y : M₁), f (x + y) = f x + f y}

source

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₂] :

is_closed {f : M₁ → M₂ | ∀ (x y : M₁), f (x * y) = f x * f y}

source

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₂.

Equations

monoid_hom_of_mem_closure_range_coe f hf = {to_fun := f, map_one' := _, map_mul' := _}

source

@[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

source

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₂.

Equations

add_monoid_hom_of_mem_closure_range_coe f hf = {to_fun := f, map_zero' := _, map_add' := _}

source

@[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))) :

⇑(add_monoid_hom_of_mem_closure_range_coe f hf) = f

source

@[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 (nhds f)) :

⇑(add_monoid_hom_of_tendsto f g h) = f

source

@[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 (nhds f)) :

⇑(monoid_hom_of_tendsto f g h) = f

source

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 (nhds f)) :

M₁ →* M₂

Construct a bundled monoid homomorphism from a pointwise limit of monoid homomorphisms.

Equations

monoid_hom_of_tendsto f g h = monoid_hom_of_mem_closure_range_coe f _

source

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 (nhds f)) :

M₁ →+ M₂

Construct a bundled additive monoid homomorphism from a pointwise limit of additive monoid homomorphisms

Equations

add_monoid_hom_of_tendsto f g h = add_monoid_hom_of_mem_closure_range_coe f _

source

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₂] :

is_closed (set.range coe_fn)

source

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₂] :

is_closed (set.range coe_fn)

source

theorem inducing.has_continuous_add {M : Type u_1} {N : Type u_2} {F : Type u_3} [has_add M] [has_add N] [add_hom_class F M N] [topological_space M] [topological_space N] [has_continuous_add N] (f : F) (hf : inducing ⇑f) :

has_continuous_add M

source

theorem inducing.has_continuous_mul {M : Type u_1} {N : Type u_2} {F : Type u_3} [has_mul M] [has_mul N] [mul_hom_class F M N] [topological_space M] [topological_space N] [has_continuous_mul N] (f : F) (hf : inducing ⇑f) :

has_continuous_mul M

source

theorem has_continuous_mul_induced {M : Type u_1} {N : Type u_2} {F : Type u_3} [has_mul M] [has_mul N] [mul_hom_class F M N] [topological_space N] [has_continuous_mul N] (f : F) :

has_continuous_mul M

source

theorem has_continuous_add_induced {M : Type u_1} {N : Type u_2} {F : Type u_3} [has_add M] [has_add N] [add_hom_class F M N] [topological_space N] [has_continuous_add N] (f : F) :

has_continuous_add M

source

@[protected, instance]

def subsemigroup.has_continuous_mul {M : Type u_4} [topological_space M] [semigroup M] [has_continuous_mul M] (S : subsemigroup M) :

has_continuous_mul ↥S

source

@[protected, instance]

def add_subsemigroup.has_continuous_add {M : Type u_4} [topological_space M] [add_semigroup M] [has_continuous_add M] (S : add_subsemigroup M) :

has_continuous_add ↥S

source

@[protected, instance]

def submonoid.has_continuous_mul {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (S : submonoid M) :

has_continuous_mul ↥S

source

@[protected, instance]

def add_submonoid.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

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

s.topological_closure = {carrier := closure ↑s, mul_mem' := _, one_mem' := _}

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.

Equations

s.topological_closure = {carrier := closure ↑s, add_mem' := _, zero_mem' := _}

source

theorem add_submonoid.le_topological_closure {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] (s : add_submonoid M) :

s ≤ s.topological_closure

source

theorem submonoid.le_topological_closure {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (s : submonoid M) :

s ≤ s.topological_closure

source

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) :

is_closed ↑(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 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

source

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) :

comm_monoid ↥(s.topological_closure)

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 := _}

source

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) :

add_comm_monoid ↥(s.topological_closure)

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 := _}

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 ∈ nhds 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 ∈ nhds 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 ∈ nhds 0) :

∃ (V : set M) (H : V ∈ nhds 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 ∈ nhds 1) :

∃ (V : set M) (H : V ∈ nhds 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 ∈ nhds 1) :

∃ (V : set M) (H : V ∈ nhds 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 ∈ nhds 0) :

∃ (V : set M) (H : V ∈ nhds 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 ∈ nhds 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 ∈ nhds 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 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)

source

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)

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 (nhds (a i))) → filter.tendsto (λ (b : α), (list.map (λ (c : ι), f c b) l).prod) x (nhds (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 (nhds (a i))) → filter.tendsto (λ (b : α), (list.map (λ (c : ι), f c b) l).sum) x (nhds (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_on_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 ι) {t : set X} (h : ∀ (i : ι), i ∈ l → continuous_on (f i) t) :

continuous_on (λ (a : X), (list.map (λ (i : ι), f i a) l).prod) t

source

theorem continuous_on_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 ι) {t : set X} (h : ∀ (i : ι), i ∈ l → continuous_on (f i) t) :

continuous_on (λ (a : X), (list.map (λ (i : ι), f i a) l).sum) t

source

@[continuity]

theorem continuous_pow {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (n : ℕ) :

continuous (λ (a : M), a ^ n)

source

@[continuity]

theorem continuous_nsmul {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] (n : ℕ) :

continuous (λ (a : M), n • a)

source

@[protected, instance]

def add_monoid.has_continuous_const_smul_nat {A : Type u_1} [add_monoid A] [topological_space A] [has_continuous_add A] :

has_continuous_const_smul ℕ A

source

@[protected, instance]

def add_monoid.has_continuous_smul_nat {A : Type u_1} [add_monoid A] [topological_space A] [has_continuous_add A] :

has_continuous_smul ℕ A

source

@[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)

source

@[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)

source

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

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_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

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 (nhds x)) (n : ℕ) :

filter.tendsto (λ (x : α), f x ^ n) l (nhds (x ^ n))

source

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 (nhds x)) (n : ℕ) :

filter.tendsto (λ (x : α), n • f x) l (nhds (n • x))

source

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

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_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

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

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

source

theorem filter.tendsto_cocompact_mul_left {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {a b : M} (ha : b * a = 1) :

filter.tendsto (λ (x : M), a * x) (filter.cocompact M) (filter.cocompact M)

Left-multiplication by a left-invertible element of a topological monoid is proper, i.e., inverse images of compact sets are compact.

source

theorem filter.tendsto_cocompact_mul_right {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {a b : M} (ha : a * b = 1) :

filter.tendsto (λ (x : M), x * a) (filter.cocompact M) (filter.cocompact M)

Right-multiplication by a right-invertible element of a topological monoid is proper, i.e., inverse images of compact sets are compact.

source

@[protected, instance]

def is_scalar_tower.has_continuous_const_smul {R : Type u_1} {A : Type u_2} [monoid A] [has_smul R A] [is_scalar_tower R A A] [topological_space A] [has_continuous_mul A] :

has_continuous_const_smul R A

If R acts on A via A, then continuous multiplication implies continuous scalar multiplication by constants.

Notably, this instances applies when R = A, or when [algebra R A] is available.

source

@[protected, instance]

def vadd_assoc_class.has_continuous_const_vadd {R : Type u_1} {A : Type u_2} [add_monoid A] [has_vadd R A] [vadd_assoc_class R A A] [topological_space A] [has_continuous_add A] :

has_continuous_const_vadd R A

If R acts on A via A, then continuous addition implies continuous affine addition by constants.

source

@[protected, instance]

def smul_comm_class.has_continuous_const_smul {R : Type u_1} {A : Type u_2} [monoid A] [has_smul R A] [smul_comm_class R A A] [topological_space A] [has_continuous_mul A] :

has_continuous_const_smul R A

If the action of R on A commutes with left-multiplication, then continuous multiplication implies continuous scalar multiplication by constants.

Notably, this instances applies when R = Aᵐᵒᵖ

source

@[protected, instance]

def vadd_comm_class.has_continuous_const_vadd {R : Type u_1} {A : Type u_2} [add_monoid A] [has_vadd R A] [vadd_comm_class R A A] [topological_space A] [has_continuous_add A] :

has_continuous_const_vadd R A

If the action of R on A commutes with left-addition, then continuous addition implies continuous affine addition by constants.

Notably, this instances applies when R = Aᵃᵒᵖ.

source

@[protected, instance]

def mul_opposite.has_continuous_mul {α : Type u_2} [topological_space α] [has_mul α] [has_continuous_mul α] :

has_continuous_mul αᵐᵒᵖ

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

source

@[protected, instance]

def add_opposite.has_continuous_add {α : Type u_2} [topological_space α] [has_add α] [has_continuous_add α] :

has_continuous_add αᵃᵒᵖ

If addition is continuous in α, then it also is in αᵃᵒᵖ.

source

@[protected, instance]

def units.has_continuous_mul {α : Type u_2} [topological_space α] [monoid α] [has_continuous_mul α] :

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.

source

@[protected, instance]

def add_units.has_continuous_add {α : Type u_2} [topological_space α] [add_monoid α] [has_continuous_add α] :

has_continuous_add (add_units α)

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.

source

theorem continuous.units_map {M : Type u_4} {N : Type u_5} [monoid M] [monoid N] [topological_space M] [topological_space N] (f : M →* N) (hf : continuous ⇑f) :

continuous ⇑(units.map f)

source

theorem continuous.add_units_map {M : Type u_4} {N : Type u_5} [add_monoid M] [add_monoid N] [topological_space M] [topological_space N] (f : M →+ N) (hf : continuous ⇑f) :

continuous ⇑(add_units.map f)

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 ∈ nhds 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 ∈ nhds 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 (nhds (a i))) → filter.tendsto (λ (b : α), (multiset.map (λ (c : ι), f c b) s).sum) x (nhds (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 (nhds (a i))) → filter.tendsto (λ (b : α), (multiset.map (λ (c : ι), f c b) s).prod) x (nhds (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 (nhds (a i))) → filter.tendsto (λ (b : α), s.sum (λ (c : ι), f c b)) x (nhds (s.sum (λ (c : ι), 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 (nhds (a i))) → filter.tendsto (λ (b : α), s.prod (λ (c : ι), f c b)) x (nhds (s.prod (λ (c : ι), a c)))

source

@[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)

source

@[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)

source

theorem continuous_on_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 ι) {t : set X} :

(∀ (i : ι), i ∈ s → continuous_on (f i) t) → continuous_on (λ (a : X), (multiset.map (λ (i : ι), f i a) s).sum) t

source

theorem continuous_on_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 ι) {t : set X} :

(∀ (i : ι), i ∈ s → continuous_on (f i) t) → continuous_on (λ (a : X), (multiset.map (λ (i : ι), f i a) s).prod) t

source

@[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), s.prod (λ (i : ι), f i a))

source

@[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), s.sum (λ (i : ι), f i a))

source

theorem continuous_on_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 ι) {t : set X} :

(∀ (i : ι), i ∈ s → continuous_on (f i) t) → continuous_on (λ (a : X), s.sum (λ (i : ι), f i a)) t

source

theorem continuous_on_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 ι) {t : set X} :

(∀ (i : ι), i ∈ s → continuous_on (f i) t) → continuous_on (λ (a : X), s.prod (λ (i : ι), f i a)) t

source

theorem eventually_eq_prod {ι : Type u_1} {X : Type u_2} {M : Type u_3} [comm_monoid M] {s : finset ι} {l : filter X} {f g : ι → X → M} (hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i) :

s.prod (λ (i : ι), f i) =ᶠ[l] s.prod (λ (i : ι), g i)

source

theorem eventually_eq_sum {ι : Type u_1} {X : Type u_2} {M : Type u_3} [add_comm_monoid M] {s : finset ι} {l : filter X} {f g : ι → X → M} (hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i) :

s.sum (λ (i : ι), f i) =ᶠ[l] s.sum (λ (i : ι), g i)

source

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 nhds x₀, function.mul_support (λ (i : ι), f i x) ⊆ ↑I

source

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 nhds x₀, function.support (λ (i : ι), f i x) ⊆ ↑I

source

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) :

∃ (s : finset ι), ∀ᶠ (y : X) in nhds x, finsum (λ (i : ι), f i y) = s.sum (λ (i : ι), f i y)

source

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) :

∃ (s : finset ι), ∀ᶠ (y : X) in nhds x, finprod (λ (i : ι), f i y) = s.prod (λ (i : ι), f i y)

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), finprod (λ (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), finsum (λ (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), finprod (λ (i : ι), finprod (λ (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), finsum (λ (i : ι), finsum (λ (hi : p i), f i x)))

source

@[protected, instance]

def additive.has_continuous_add {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] :

has_continuous_add (additive M)

source

@[protected, instance]

def multiplicative.has_continuous_mul {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] :

has_continuous_mul (multiplicative M)

source

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) :

has_continuous_mul M

source

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) :

has_continuous_add M

source

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) :

has_continuous_mul M

source

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) :

has_continuous_add M

source

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) :

has_continuous_mul M

source

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) :

has_continuous_add M

source

@[protected]

def continuous_map.mul_right {X : Type u_3} [topological_space X] [has_mul X] [has_continuous_mul X] (x : X) :

C(X, X)

The continuous map λ y, y * x

Equations

continuous_map.mul_right x = {to_fun := λ (b : X), b * x, continuous_to_fun := _}

source

@[protected]

def continuous_map.add_right {X : Type u_3} [topological_space X] [has_add X] [has_continuous_add X] (x : X) :

C(X, X)

The continuous map `λ y, y + x

Equations

continuous_map.add_right x = {to_fun := λ (b : X), b + x, continuous_to_fun := _}

source

@[simp]

theorem continuous_map.coe_add_right {X : Type u_3} [topological_space X] [has_add X] [has_continuous_add X] (x : X) :

⇑(continuous_map.add_right x) = λ (y : X), y + x

source

@[simp]

theorem continuous_map.coe_mul_right {X : Type u_3} [topological_space X] [has_mul X] [has_continuous_mul X] (x : X) :

⇑(continuous_map.mul_right x) = λ (y : X), y * x

source

@[protected]

def continuous_map.mul_left {X : Type u_3} [topological_space X] [has_mul X] [has_continuous_mul X] (x : X) :

C(X, X)

The continuous map λ y, x * y

Equations

continuous_map.mul_left x = {to_fun := λ (b : X), x * b, continuous_to_fun := _}

source

@[protected]

def continuous_map.add_left {X : Type u_3} [topological_space X] [has_add X] [has_continuous_add X] (x : X) :

C(X, X)

The continuous map `λ y, x + y

Equations

continuous_map.add_left x = {to_fun := λ (b : X), x + b, continuous_to_fun := _}

source

@[simp]

theorem continuous_map.coe_mul_left {X : Type u_3} [topological_space X] [has_mul X] [has_continuous_mul X] (x : X) :

⇑(continuous_map.mul_left x) = λ (y : X), x * y

source

@[simp]

theorem continuous_map.coe_add_left {X : Type u_3} [topological_space X] [has_add X] [has_continuous_add X] (x : X) :

⇑(continuous_map.add_left x) = λ (y : X), x + y

mathlib3 documentation

Theory of topological monoids #