Theory of topological monoids

In this file we define mixin classes ContinuousMul and ContinuousAdd. While in many applications the underlying type is a monoid (multiplicative or additive), we do not require this in the definitions.

theorem continuous_zero {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Zero M] : Continuous 0

theorem continuous_one {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [One M] : Continuous 1

class ContinuousAdd (M : Type u) [TopologicalSpace M] [Add M] : Prop

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 AddMonoid M and ContinuousAdd M.

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

• continuous_add : Continuous fun (p : M × M) => p.1 + p.2

class ContinuousMul (M : Type u) [TopologicalSpace M] [Mul M] : Prop

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 ContinuousMul M.

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

• continuous_mul : Continuous fun (p : M × M) => p.1 * p.2

instance instContinuousAddOrderDualInstTopologicalSpaceOrderDualInstAddOrderDual {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] : ContinuousAdd Mᵒᵈ

Equations

• (_ : ContinuousAdd Mᵒᵈ) = inst

instance instContinuousMulOrderDualInstTopologicalSpaceOrderDualInstMulOrderDual {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] : ContinuousMul Mᵒᵈ

Equations

• (_ : ContinuousMul Mᵒᵈ) = inst

theorem continuous_add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] : Continuous fun (p : M × M) => p.1 + p.2

theorem continuous_mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] : Continuous fun (p : M × M) => p.1 * p.2

instance ContinuousAdd.to_continuousVAdd {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] : ContinuousVAdd M M

Equations

• (_ : ContinuousVAdd M M) = (_ : ContinuousVAdd M M)

instance ContinuousMul.to_continuousSMul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] : ContinuousSMul M M

Equations

• (_ : ContinuousSMul M M) = (_ : ContinuousSMul M M)

instance ContinuousAdd.to_continuousVAdd_op {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] : ContinuousVAdd Mᵃᵒᵖ M

Equations

• (_ : ContinuousVAdd Mᵃᵒᵖ M) = (_ : ContinuousVAdd Mᵃᵒᵖ M)

instance ContinuousMul.to_continuousSMul_op {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] : ContinuousSMul Mᵐᵒᵖ M

Equations

• (_ : ContinuousSMul Mᵐᵒᵖ M) = (_ : ContinuousSMul Mᵐᵒᵖ M)

theorem Continuous.add {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Add M] [ContinuousAdd M] {f : X → M} {g : X → M} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : X) => f x + g x

theorem Continuous.mul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Mul M] [ContinuousMul M] {f : X → M} {g : X → M} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : X) => f x * g x

theorem continuous_add_left {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] (a : M) : Continuous fun (b : M) => a + b

theorem continuous_mul_left {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a : M) : Continuous fun (b : M) => a * b

theorem continuous_add_right {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] (a : M) : Continuous fun (b : M) => b + a

theorem continuous_mul_right {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a : M) : Continuous fun (b : M) => b * a

theorem ContinuousOn.add {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Add M] [ContinuousAdd M] {f : X → M} {g : X → M} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (x : X) => f x + g x) s

theorem ContinuousOn.mul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Mul M] [ContinuousMul M] {f : X → M} {g : X → M} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (x : X) => f x * g x) s

theorem tendsto_add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] {a : M} {b : M} : Filter.Tendsto (fun (p : M × M) => p.1 + p.2) (nhds (a, b)) (nhds (a + b))

theorem tendsto_mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] {a : M} {b : M} : Filter.Tendsto (fun (p : M × M) => p.1 * p.2) (nhds (a, b)) (nhds (a * b))

theorem Filter.Tendsto.add {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] {f : α → M} {g : α → M} {x : Filter α} {a : M} {b : M} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.Tendsto (fun (x : α) => f x + g x) x (nhds (a + b))

theorem Filter.Tendsto.mul {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] {f : α → M} {g : α → M} {x : Filter α} {a : M} {b : M} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.Tendsto (fun (x : α) => f x * g x) x (nhds (a * b))

theorem Filter.Tendsto.const_add {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] (b : M) {c : M} {f : α → M} {l : Filter α} (h : Filter.Tendsto (fun (k : α) => f k) l (nhds c)) : Filter.Tendsto (fun (k : α) => b + f k) l (nhds (b + c))

theorem Filter.Tendsto.const_mul {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (b : M) {c : M} {f : α → M} {l : Filter α} (h : Filter.Tendsto (fun (k : α) => f k) l (nhds c)) : Filter.Tendsto (fun (k : α) => b * f k) l (nhds (b * c))

theorem Filter.Tendsto.add_const {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] (b : M) {c : M} {f : α → M} {l : Filter α} (h : Filter.Tendsto (fun (k : α) => f k) l (nhds c)) : Filter.Tendsto (fun (k : α) => f k + b) l (nhds (c + b))

theorem Filter.Tendsto.mul_const {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (b : M) {c : M} {f : α → M} {l : Filter α} (h : Filter.Tendsto (fun (k : α) => f k) l (nhds c)) : Filter.Tendsto (fun (k : α) => f k * b) l (nhds (c * b))

theorem le_nhds_add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] (a : M) (b : M) : nhds a + nhds b ≤ nhds (a + b)

theorem le_nhds_mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a : M) (b : M) : nhds a * nhds b ≤ nhds (a * b)

@[simp]

theorem nhds_zero_add_nhds {M : Type u_6} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] (a : M) : nhds 0 + nhds a = nhds a

@[simp]

theorem nhds_one_mul_nhds {M : Type u_6} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) : nhds 1 * nhds a = nhds a

@[simp]

theorem nhds_add_nhds_zero {M : Type u_6} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] (a : M) : nhds a + nhds 0 = nhds a

@[simp]

theorem nhds_mul_nhds_one {M : Type u_6} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) : nhds a * nhds 1 = nhds a

theorem Filter.TendstoNhdsWithinIoi.const_mul {α : Type u_2} {𝕜 : Type u_6} [Preorder 𝕜] [Zero 𝕜] [Mul 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b : 𝕜} {c : 𝕜} (hb : 0 < b) [PosMulStrictMono 𝕜] [PosMulReflectLT 𝕜] (h : Filter.Tendsto f l (nhdsWithin c (Set.Ioi c))) : Filter.Tendsto (fun (a : α) => b * f a) l (nhdsWithin (b * c) (Set.Ioi (b * c)))

theorem Filter.TendstoNhdsWithinIio.const_mul {α : Type u_2} {𝕜 : Type u_6} [Preorder 𝕜] [Zero 𝕜] [Mul 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b : 𝕜} {c : 𝕜} (hb : 0 < b) [PosMulStrictMono 𝕜] [PosMulReflectLT 𝕜] (h : Filter.Tendsto f l (nhdsWithin c (Set.Iio c))) : Filter.Tendsto (fun (a : α) => b * f a) l (nhdsWithin (b * c) (Set.Iio (b * c)))

theorem Filter.TendstoNhdsWithinIoi.mul_const {α : Type u_2} {𝕜 : Type u_6} [Preorder 𝕜] [Zero 𝕜] [Mul 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b : 𝕜} {c : 𝕜} (hb : 0 < b) [MulPosStrictMono 𝕜] [MulPosReflectLT 𝕜] (h : Filter.Tendsto f l (nhdsWithin c (Set.Ioi c))) : Filter.Tendsto (fun (a : α) => f a * b) l (nhdsWithin (c * b) (Set.Ioi (c * b)))

theorem Filter.TendstoNhdsWithinIio.mul_const {α : Type u_2} {𝕜 : Type u_6} [Preorder 𝕜] [Zero 𝕜] [Mul 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b : 𝕜} {c : 𝕜} (hb : 0 < b) [MulPosStrictMono 𝕜] [MulPosReflectLT 𝕜] (h : Filter.Tendsto f l (nhdsWithin c (Set.Iio c))) : Filter.Tendsto (fun (a : α) => f a * b) l (nhdsWithin (c * b) (Set.Iio (c * b)))

theorem Filter.Tendsto.addUnits.proof_1 {ι : Type u_2} {N : Type u_1} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ι → AddUnits N} {r₁ : N} {r₂ : N} {l : Filter ι} [Filter.NeBot l] (h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂)) : r₁ + r₂ = 0

def Filter.Tendsto.addUnits {ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ι → AddUnits N} {r₁ : N} {r₂ : N} {l : Filter ι} [Filter.NeBot l] (h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂)) : AddUnits N

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

Equations

• Filter.Tendsto.addUnits h₁ h₂ = { val := r₁, neg := r₂, val_neg := (_ : r₁ + r₂ = 0), neg_val := (_ : r₂ + r₁ = 0) }

theorem Filter.Tendsto.addUnits.proof_2 {ι : Type u_2} {N : Type u_1} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ι → AddUnits N} {r₁ : N} {r₂ : N} {l : Filter ι} [Filter.NeBot l] (h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂)) : r₂ + r₁ = 0

@[simp]

theorem Filter.Tendsto.val_inv_units {ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → Nˣ} {r₁ : N} {r₂ : N} {l : Filter ι} [Filter.NeBot l] (h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂)) : ↑(Filter.Tendsto.units h₁ h₂)⁻¹ = r₂

@[simp]

theorem Filter.Tendsto.val_units {ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → Nˣ} {r₁ : N} {r₂ : N} {l : Filter ι} [Filter.NeBot l] (h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂)) : ↑(Filter.Tendsto.units h₁ h₂) = r₁

@[simp]

theorem Filter.Tendsto.val_neg_addUnits {ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ι → AddUnits N} {r₁ : N} {r₂ : N} {l : Filter ι} [Filter.NeBot l] (h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂)) : ↑(-Filter.Tendsto.addUnits h₁ h₂) = r₂

@[simp]

theorem Filter.Tendsto.val_addUnits {ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ι → AddUnits N} {r₁ : N} {r₂ : N} {l : Filter ι} [Filter.NeBot l] (h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂)) : ↑(Filter.Tendsto.addUnits h₁ h₂) = r₁

def Filter.Tendsto.units {ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → Nˣ} {r₁ : N} {r₂ : N} {l : Filter ι} [Filter.NeBot l] (h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂)) : Nˣ

Construct a unit from limits of units and their inverses.

Equations

• Filter.Tendsto.units h₁ h₂ = { val := r₁, inv := r₂, val_inv := (_ : r₁ * r₂ = 1), inv_val := (_ : r₂ * r₁ = 1) }

theorem ContinuousAt.add {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Add M] [ContinuousAdd M] {f : X → M} {g : X → M} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun (x : X) => f x + g x) x

theorem ContinuousAt.mul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Mul M] [ContinuousMul M] {f : X → M} {g : X → M} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun (x : X) => f x * g x) x

theorem ContinuousWithinAt.add {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Add M] [ContinuousAdd M] {f : X → M} {g : X → M} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun (x : X) => f x + g x) s x

theorem ContinuousWithinAt.mul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Mul M] [ContinuousMul M] {f : X → M} {g : X → M} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun (x : X) => f x * g x) s x

instance Prod.continuousAdd {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [Add M] [ContinuousAdd M] [TopologicalSpace N] [Add N] [ContinuousAdd N] : ContinuousAdd (M × N)

Equations

• (_ : ContinuousAdd (M × N)) = (_ : ContinuousAdd (M × N))

instance Prod.continuousMul {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [Mul M] [ContinuousMul M] [TopologicalSpace N] [Mul N] [ContinuousMul N] : ContinuousMul (M × N)

Equations

• (_ : ContinuousMul (M × N)) = (_ : ContinuousMul (M × N))

instance Pi.continuousAdd {ι : Type u_1} {C : ι → Type u_6} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Add (C i)] [∀ (i : ι), ContinuousAdd (C i)] : ContinuousAdd ((i : ι) → C i)

Equations

• (_ : ContinuousAdd ((i : ι) → C i)) = (_ : ContinuousAdd ((i : ι) → C i))

instance Pi.continuousMul {ι : Type u_1} {C : ι → Type u_6} [(i : ι) → TopologicalSpace (C i)] [(i : ι) → Mul (C i)] [∀ (i : ι), ContinuousMul (C i)] : ContinuousMul ((i : ι) → C i)

Equations

• (_ : ContinuousMul ((i : ι) → C i)) = (_ : ContinuousMul ((i : ι) → C i))

instance Pi.continuousAdd' {ι : Type u_1} {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] : ContinuousAdd (ι → M)

A version of Pi.continuousAdd for non-dependent functions. It is needed because sometimes Lean fails to use Pi.continuousAdd for non-dependent functions.

Equations

• (_ : ContinuousAdd (ι → M)) = (_ : ContinuousAdd (ι → M))

instance Pi.continuousMul' {ι : Type u_1} {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] : ContinuousMul (ι → M)

A version of Pi.continuousMul for non-dependent functions. It is needed because sometimes Lean 3 fails to use Pi.continuousMul for non-dependent functions.

Equations

• (_ : ContinuousMul (ι → M)) = (_ : ContinuousMul (ι → M))

instance continuousAdd_of_discreteTopology {N : Type u_4} [TopologicalSpace N] [Add N] [DiscreteTopology N] : ContinuousAdd N

Equations

• (_ : ContinuousAdd N) = (_ : ContinuousAdd N)

instance continuousMul_of_discreteTopology {N : Type u_4} [TopologicalSpace N] [Mul N] [DiscreteTopology N] : ContinuousMul N

Equations

• (_ : ContinuousMul N) = (_ : ContinuousMul N)

theorem ContinuousAdd.of_nhds_zero {M : Type u} [AddMonoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : M) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x₀ + x) (nhds 0)) (hright : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x + x₀) (nhds 0)) : ContinuousAdd M

theorem ContinuousMul.of_nhds_one {M : Type u} [Monoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : M) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x₀ * x) (nhds 1)) (hright : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x * x₀) (nhds 1)) : ContinuousMul M

theorem continuousAdd_of_comm_of_nhds_zero (M : Type u) [AddCommMonoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : M) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x₀ + x) (nhds 0)) : ContinuousAdd M

theorem continuousMul_of_comm_of_nhds_one (M : Type u) [CommMonoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : M) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x₀ * x) (nhds 1)) : ContinuousMul M

theorem isClosed_setOf_map_zero (M₁ : Type u_6) (M₂ : Type u_7) [TopologicalSpace M₂] [T2Space M₂] [Zero M₁] [Zero M₂] : IsClosed {f : M₁ → M₂ | f 0 = 0}

theorem isClosed_setOf_map_one (M₁ : Type u_6) (M₂ : Type u_7) [TopologicalSpace M₂] [T2Space M₂] [One M₁] [One M₂] : IsClosed {f : M₁ → M₂ | f 1 = 1}

theorem isClosed_setOf_map_add (M₁ : Type u_6) (M₂ : Type u_7) [TopologicalSpace M₂] [T2Space M₂] [Add M₁] [Add M₂] [ContinuousAdd M₂] : IsClosed {f : M₁ → M₂ | ∀ (x y : M₁), f (x + y) = f x + f y}

theorem isClosed_setOf_map_mul (M₁ : Type u_6) (M₂ : Type u_7) [TopologicalSpace M₂] [T2Space M₂] [Mul M₁] [Mul M₂] [ContinuousMul M₂] : IsClosed {f : M₁ → M₂ | ∀ (x y : M₁), f (x * y) = f x * f y}

theorem addMonoidHomOfMemClosureRangeCoe.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] {F : Type u_3} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) : { toFun := f, map_zero' := (_ : f ∈ {f : M₁ → M₂ | f 0 = 0}) }.toFun ∈ {f : M₁ → M₂ | ∀ (x y : M₁), f (x + y) = f x + f y}

def addMonoidHomOfMemClosureRangeCoe {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (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 an AddMonoidHomClass instance) to M₁ → M₂.

Equations

• One or more equations did not get rendered due to their size.

theorem addMonoidHomOfMemClosureRangeCoe.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] {F : Type u_3} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) : f ∈ {f : M₁ → M₂ | f 0 = 0}

@[simp]

theorem monoidHomOfMemClosureRangeCoe_apply {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [MulOneClass M₁] [MulOneClass M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) : ⇑(monoidHomOfMemClosureRangeCoe f hf) = f

@[simp]

theorem addMonoidHomOfMemClosureRangeCoe_apply {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) : ⇑(addMonoidHomOfMemClosureRangeCoe f hf) = f

def monoidHomOfMemClosureRangeCoe {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [MulOneClass M₁] [MulOneClass M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (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 MonoidHomClass instance) to M₁ → M₂.

Equations

• One or more equations did not get rendered due to their size.

def addMonoidHomOfTendsto {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [Filter.NeBot l] (h : Filter.Tendsto (fun (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

• addMonoidHomOfTendsto f g h = addMonoidHomOfMemClosureRangeCoe f (_ : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x))

theorem addMonoidHomOfTendsto.proof_1 {α : Type u_4} {M₁ : Type u_1} {M₂ : Type u_2} [TopologicalSpace M₂] {F : Type u_3} [FunLike F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)

@[simp]

theorem addMonoidHomOfTendsto_apply {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) : ⇑(addMonoidHomOfTendsto f g h) = f

@[simp]

theorem monoidHomOfTendsto_apply {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [MulOneClass M₁] [MulOneClass M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) : ⇑(monoidHomOfTendsto f g h) = f

def monoidHomOfTendsto {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [MulOneClass M₁] [MulOneClass M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) : M₁ →* M₂

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

Equations

• monoidHomOfTendsto f g h = monoidHomOfMemClosureRangeCoe f (_ : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x))

theorem AddMonoidHom.isClosed_range_coe (M₁ : Type u_6) (M₂ : Type u_7) [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] : IsClosed (Set.range DFunLike.coe)

theorem MonoidHom.isClosed_range_coe (M₁ : Type u_6) (M₂ : Type u_7) [TopologicalSpace M₂] [T2Space M₂] [MulOneClass M₁] [MulOneClass M₂] [ContinuousMul M₂] : IsClosed (Set.range DFunLike.coe)

theorem Inducing.continuousAdd {M : Type u_6} {N : Type u_7} {F : Type u_8} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] (f : F) (hf : Inducing ⇑f) : ContinuousAdd M

theorem Inducing.continuousMul {M : Type u_6} {N : Type u_7} {F : Type u_8} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousMul N] (f : F) (hf : Inducing ⇑f) : ContinuousMul M

theorem continuousAdd_induced {M : Type u_6} {N : Type u_7} {F : Type u_8} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] [TopologicalSpace N] [ContinuousAdd N] (f : F) : ContinuousAdd M

theorem continuousMul_induced {M : Type u_6} {N : Type u_7} {F : Type u_8} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [TopologicalSpace N] [ContinuousMul N] (f : F) : ContinuousMul M

instance AddSubsemigroup.continuousAdd {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (S : AddSubsemigroup M) : ContinuousAdd ↥S

Equations

• (_ : ContinuousAdd ↥S) = (_ : ContinuousAdd ↥S)

instance Subsemigroup.continuousMul {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] (S : Subsemigroup M) : ContinuousMul ↥S

Equations

• (_ : ContinuousMul ↥S) = (_ : ContinuousMul ↥S)

instance AddSubmonoid.continuousAdd {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (S : AddSubmonoid M) : ContinuousAdd ↥S

Equations

• (_ : ContinuousAdd ↥S) = (_ : ContinuousAdd ↥S.toAddSubsemigroup)

instance Submonoid.continuousMul {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (S : Submonoid M) : ContinuousMul ↥S

Equations

• (_ : ContinuousMul ↥S) = (_ : ContinuousMul ↥S.toSubsemigroup)

theorem AddSubmonoid.top_closure_add_self_subset {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) : closure ↑s + closure ↑s ⊆ closure ↑s

theorem Submonoid.top_closure_mul_self_subset {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) : closure ↑s * closure ↑s ⊆ closure ↑s

theorem AddSubmonoid.top_closure_add_self_eq {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) : closure ↑s + closure ↑s = closure ↑s

theorem Submonoid.top_closure_mul_self_eq {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) : closure ↑s * closure ↑s = closure ↑s

theorem AddSubmonoid.topologicalClosure.proof_2 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] (s : AddSubmonoid M) : 0 ∈ closure ↑s

def AddSubmonoid.topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) : AddSubmonoid M

The (topological-space) closure of an additive submonoid of a space M with ContinuousAdd is itself an additive submonoid.

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubmonoid.topologicalClosure.proof_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) : ∀ {a b : M}, a ∈ closure ↑s → b ∈ closure ↑s → a + b ∈ closure ↑s

def Submonoid.topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) : Submonoid M

The (topological-space) closure of a submonoid of a space M with ContinuousMul is itself a submonoid.

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubmonoid.coe_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) : ↑(AddSubmonoid.topologicalClosure s) = closure ↑s

theorem Submonoid.coe_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) : ↑(Submonoid.topologicalClosure s) = closure ↑s

theorem AddSubmonoid.le_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) : s ≤ AddSubmonoid.topologicalClosure s

theorem Submonoid.le_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) : s ≤ Submonoid.topologicalClosure s

theorem AddSubmonoid.isClosed_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) : IsClosed ↑(AddSubmonoid.topologicalClosure s)

theorem Submonoid.isClosed_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) : IsClosed ↑(Submonoid.topologicalClosure s)

theorem AddSubmonoid.topologicalClosure_minimal {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) {t : AddSubmonoid M} (h : s ≤ t) (ht : IsClosed ↑t) : AddSubmonoid.topologicalClosure s ≤ t

theorem Submonoid.topologicalClosure_minimal {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) {t : Submonoid M} (h : s ≤ t) (ht : IsClosed ↑t) : Submonoid.topologicalClosure s ≤ t

theorem AddSubmonoid.addCommMonoidTopologicalClosure.proof_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] [T2Space M] (s : AddSubmonoid M) (hs : ∀ (x y : ↥s), x + y = y + x) : ∀ (x x_1 : ↥(AddSubmonoid.topologicalClosure s)), x + x_1 = x_1 + x

def AddSubmonoid.addCommMonoidTopologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] [T2Space M] (s : AddSubmonoid M) (hs : ∀ (x y : ↥s), x + y = y + x) : AddCommMonoid ↥(AddSubmonoid.topologicalClosure s)

If a submonoid of an additive topological monoid is commutative, then so is its topological closure.

Equations

• One or more equations did not get rendered due to their size.

abbrev AddSubmonoid.addCommMonoidTopologicalClosure.match_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) (motive : ↥(AddSubmonoid.topologicalClosure s) → Prop) : ∀ (x : ↥(AddSubmonoid.topologicalClosure s)), (∀ (y : M) (hy : y ∈ AddSubmonoid.topologicalClosure s), motive { val := y, property := hy }) → motive x

Equations

• (_ : motive x) = (_ : motive x)

def Submonoid.commMonoidTopologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] [T2Space M] (s : Submonoid M) (hs : ∀ (x y : ↥s), x * y = y * x) : CommMonoid ↥(Submonoid.topologicalClosure s)

If a submonoid of a topological monoid is commutative, then so is its topological closure.

Equations

• Submonoid.commMonoidTopologicalClosure s hs = let src := Submonoid.toMonoid (Submonoid.topologicalClosure s); CommMonoid.mk (_ : ∀ (x x_1 : ↥(Submonoid.topologicalClosure s)), x * x_1 = x_1 * x)

theorem exists_open_nhds_zero_half {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {s : Set M} (hs : s ∈ nhds 0) : ∃ (V : Set M), IsOpen V ∧ 0 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s

theorem exists_open_nhds_one_split {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {s : Set M} (hs : s ∈ nhds 1) : ∃ (V : Set M), IsOpen V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

abbrev exists_nhds_zero_half.match_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] {s : Set M} (motive : (∃ (V : Set M), IsOpen V ∧ 0 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s) → Prop) : ∀ (x : ∃ (V : Set M), IsOpen V ∧ 0 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s), (∀ (V : Set M) (Vo : IsOpen V) (V1 : 0 ∈ V) (hV : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s), motive (_ : ∃ (V : Set M), IsOpen V ∧ 0 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem exists_nhds_zero_half {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {s : Set M} (hs : s ∈ nhds 0) : ∃ V ∈ nhds 0, ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s

theorem exists_nhds_one_split {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {s : Set M} (hs : s ∈ nhds 1) : ∃ V ∈ nhds 1, ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

theorem exists_nhds_zero_quarter {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {u : Set M} (hu : u ∈ nhds 0) : ∃ V ∈ nhds 0, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v + w + s + t ∈ u

theorem exists_nhds_one_split4 {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {u : Set M} (hu : u ∈ nhds 1) : ∃ V ∈ nhds 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

theorem exists_open_nhds_zero_add_subset {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {U : Set M} (hU : U ∈ nhds 0) : ∃ (V : Set M), IsOpen V ∧ 0 ∈ V ∧ V + V ⊆ U

Given an open neighborhood U of 0 there is an open neighborhood V of 0 such that V + V ⊆ U.

theorem exists_open_nhds_one_mul_subset {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {U : Set M} (hU : U ∈ nhds 1) : ∃ (V : Set M), IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U

Given a neighborhood U of 1 there is an open neighborhood V of 1 such that VV ⊆ U.

theorem IsCompact.add {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {s : Set M} {t : Set M} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s + t)

theorem IsCompact.mul {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {s : Set M} {t : Set M} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s * t)

theorem tendsto_list_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι) : (∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => List.sum (List.map (fun (c : ι) => f c b) l)) x (nhds (List.sum (List.map a l)))

abbrev tendsto_list_sum.match_1 {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] {f : ι → α → M} {x : Filter α} {a : ι → M} (motive : (x_1 : List ι) → (∀ i ∈ x_1, Filter.Tendsto (f i) x (nhds (a i))) → Prop) : ∀ (x_1 : List ι) (x_2 : ∀ i ∈ x_1, Filter.Tendsto (f i) x (nhds (a i))), (∀ (x : ∀ i ∈ [], Filter.Tendsto (f i) x (nhds (a i))), motive [] x) → (∀ (f_1 : ι) (l : List ι) (h : ∀ i ∈ f_1 :: l, Filter.Tendsto (f i) x (nhds (a i))), motive (f_1 :: l) h) → motive x_1 x_2

Equations

• (_ : motive x✝ x) = (_ : motive x✝ x)

theorem tendsto_list_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι) : (∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => List.prod (List.map (fun (c : ι) => f c b) l)) x (nhds (List.prod (List.map a l)))

theorem continuous_list_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : ι → X → M} (l : List ι) (h : ∀ i ∈ l, Continuous (f i)) : Continuous fun (a : X) => List.sum (List.map (fun (i : ι) => f i a) l)

theorem continuous_list_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : ι → X → M} (l : List ι) (h : ∀ i ∈ l, Continuous (f i)) : Continuous fun (a : X) => List.prod (List.map (fun (i : ι) => f i a) l)

theorem continuousOn_list_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : ι → X → M} (l : List ι) {t : Set X} (h : ∀ i ∈ l, ContinuousOn (f i) t) : ContinuousOn (fun (a : X) => List.sum (List.map (fun (i : ι) => f i a) l)) t

theorem continuousOn_list_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : ι → X → M} (l : List ι) {t : Set X} (h : ∀ i ∈ l, ContinuousOn (f i) t) : ContinuousOn (fun (a : X) => List.prod (List.map (fun (i : ι) => f i a) l)) t

theorem continuous_nsmul {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (n : ℕ) : Continuous fun (a : M) => n • a

abbrev continuous_nsmul.match_1 (motive : ℕ → Prop) : ∀ (x : ℕ), (Unit → motive 0) → (∀ (k : ℕ), motive (Nat.succ k)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem continuous_pow {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (n : ℕ) : Continuous fun (a : M) => a ^ n

instance AddMonoid.continuousConstSMul_nat {A : Type u_6} [AddMonoid A] [TopologicalSpace A] [ContinuousAdd A] : ContinuousConstSMul ℕ A

Equations

• (_ : ContinuousConstSMul ℕ A) = (_ : ContinuousConstSMul ℕ A)

instance AddMonoid.continuousSMul_nat {A : Type u_6} [AddMonoid A] [TopologicalSpace A] [ContinuousAdd A] : ContinuousSMul ℕ A

Equations

• (_ : ContinuousSMul ℕ A) = (_ : ContinuousSMul ℕ A)

theorem Continuous.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : X → M} (h : Continuous f) (n : ℕ) : Continuous fun (b : X) => n • f b

theorem Continuous.pow {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : X → M} (h : Continuous f) (n : ℕ) : Continuous fun (b : X) => f b ^ n

theorem continuousOn_nsmul {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {s : Set M} (n : ℕ) : ContinuousOn (fun (x : M) => n • x) s

theorem continuousOn_pow {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {s : Set M} (n : ℕ) : ContinuousOn (fun (x : M) => x ^ n) s

theorem continuousAt_nsmul {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (x : M) (n : ℕ) : ContinuousAt (fun (x : M) => n • x) x

theorem continuousAt_pow {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (x : M) (n : ℕ) : ContinuousAt (fun (x : M) => x ^ n) x

theorem Filter.Tendsto.nsmul {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {l : Filter α} {f : α → M} {x : M} (hf : Filter.Tendsto f l (nhds x)) (n : ℕ) : Filter.Tendsto (fun (x : α) => n • f x) l (nhds (n • x))

theorem Filter.Tendsto.pow {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {l : Filter α} {f : α → M} {x : M} (hf : Filter.Tendsto f l (nhds x)) (n : ℕ) : Filter.Tendsto (fun (x : α) => f x ^ n) l (nhds (x ^ n))

theorem ContinuousWithinAt.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : X → M} {x : X} {s : Set X} (hf : ContinuousWithinAt f s x) (n : ℕ) : ContinuousWithinAt (fun (x : X) => n • f x) s x

theorem ContinuousWithinAt.pow {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : X → M} {x : X} {s : Set X} (hf : ContinuousWithinAt f s x) (n : ℕ) : ContinuousWithinAt (fun (x : X) => f x ^ n) s x

theorem ContinuousAt.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : X → M} {x : X} (hf : ContinuousAt f x) (n : ℕ) : ContinuousAt (fun (x : X) => n • f x) x

theorem ContinuousAt.pow {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : X → M} {x : X} (hf : ContinuousAt f x) (n : ℕ) : ContinuousAt (fun (x : X) => f x ^ n) x

theorem ContinuousOn.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : X → M} {s : Set X} (hf : ContinuousOn f s) (n : ℕ) : ContinuousOn (fun (x : X) => n • f x) s

theorem ContinuousOn.pow {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : X → M} {s : Set X} (hf : ContinuousOn f s) (n : ℕ) : ContinuousOn (fun (x : X) => f x ^ n) s

theorem Filter.tendsto_cocompact_mul_left {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {a : M} {b : M} (ha : b * a = 1) : Filter.Tendsto (fun (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.

theorem Filter.tendsto_cocompact_mul_right {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {a : M} {b : M} (ha : a * b = 1) : Filter.Tendsto (fun (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.

instance VAddAssocClass.continuousConstVAdd {R : Type u_6} {A : Type u_7} [AddMonoid A] [VAdd R A] [VAddAssocClass R A A] [TopologicalSpace A] [ContinuousAdd A] : ContinuousConstVAdd R A

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

Equations

• (_ : ContinuousConstVAdd R A) = (_ : ContinuousConstVAdd R A)

instance IsScalarTower.continuousConstSMul {R : Type u_6} {A : Type u_7} [Monoid A] [SMul R A] [IsScalarTower R A A] [TopologicalSpace A] [ContinuousMul A] : ContinuousConstSMul 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.

Equations

• (_ : ContinuousConstSMul R A) = (_ : ContinuousConstSMul R A)

instance VAddCommClass.continuousConstVAdd {R : Type u_6} {A : Type u_7} [AddMonoid A] [VAdd R A] [VAddCommClass R A A] [TopologicalSpace A] [ContinuousAdd A] : ContinuousConstVAdd 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ᵃᵒᵖ.

Equations

• (_ : ContinuousConstVAdd R A) = (_ : ContinuousConstVAdd R A)

instance SMulCommClass.continuousConstSMul {R : Type u_6} {A : Type u_7} [Monoid A] [SMul R A] [SMulCommClass R A A] [TopologicalSpace A] [ContinuousMul A] : ContinuousConstSMul 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ᵐᵒᵖ.

Equations

• (_ : ContinuousConstSMul R A) = (_ : ContinuousConstSMul R A)

instance AddOpposite.instContinuousAddAddOppositeInstTopologicalSpaceAddOppositeAdd {α : Type u_2} [TopologicalSpace α] [Add α] [ContinuousAdd α] : ContinuousAdd αᵃᵒᵖ

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

Equations

• (_ : ContinuousAdd αᵃᵒᵖ) = (_ : ContinuousAdd αᵃᵒᵖ)

instance MulOpposite.instContinuousMulMulOppositeInstTopologicalSpaceMulOppositeMul {α : Type u_2} [TopologicalSpace α] [Mul α] [ContinuousMul α] : ContinuousMul αᵐᵒᵖ

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

Equations

• (_ : ContinuousMul αᵐᵒᵖ) = (_ : ContinuousMul αᵐᵒᵖ)

instance AddUnits.instContinuousAddAddUnitsInstTopologicalSpaceAddUnitsToAddInstAddZeroClass {α : Type u_2} [TopologicalSpace α] [AddMonoid α] [ContinuousAdd α] : ContinuousAdd (AddUnits α)

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 ContinuousNeg has not yet been defined.

Equations

• (_ : ContinuousAdd (AddUnits α)) = (_ : ContinuousAdd (AddUnits α))

instance Units.instContinuousMulUnitsInstTopologicalSpaceUnitsToMulInstMulOneClass {α : Type u_2} [TopologicalSpace α] [Monoid α] [ContinuousMul α] : ContinuousMul αˣ

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 ContinuousInv has not yet been defined.

Equations

• (_ : ContinuousMul αˣ) = (_ : ContinuousMul αˣ)

theorem Continuous.addUnits_map {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] [TopologicalSpace M] [TopologicalSpace N] (f : M →+ N) (hf : Continuous ⇑f) : Continuous ⇑(AddUnits.map f)

theorem Continuous.units_map {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N] (f : M →* N) (hf : Continuous ⇑f) : Continuous ⇑(Units.map f)

theorem AddSubmonoid.mem_nhds_zero {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] (S : AddSubmonoid M) (oS : IsOpen ↑S) : ↑S ∈ nhds 0

theorem Submonoid.mem_nhds_one {M : Type u_3} [TopologicalSpace M] [CommMonoid M] (S : Submonoid M) (oS : IsOpen ↑S) : ↑S ∈ nhds 1

theorem tendsto_multiset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => Multiset.sum (Multiset.map (fun (c : ι) => f c b) s)) x (nhds (Multiset.sum (Multiset.map a s)))

theorem tendsto_multiset_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => Multiset.prod (Multiset.map (fun (c : ι) => f c b) s)) x (nhds (Multiset.prod (Multiset.map a s)))

theorem tendsto_finset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => Finset.sum s fun (c : ι) => f c b) x (nhds (Finset.sum s fun (c : ι) => a c))

theorem tendsto_finset_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => Finset.prod s fun (c : ι) => f c b) x (nhds (Finset.prod s fun (c : ι) => a c))

theorem continuous_multiset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Multiset ι) : (∀ i ∈ s, Continuous (f i)) → Continuous fun (a : X) => Multiset.sum (Multiset.map (fun (i : ι) => f i a) s)

theorem continuous_multiset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Multiset ι) : (∀ i ∈ s, Continuous (f i)) → Continuous fun (a : X) => Multiset.prod (Multiset.map (fun (i : ι) => f i a) s)

theorem continuousOn_multiset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Multiset ι) {t : Set X} : (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun (a : X) => Multiset.sum (Multiset.map (fun (i : ι) => f i a) s)) t

theorem continuousOn_multiset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Multiset ι) {t : Set X} : (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun (a : X) => Multiset.prod (Multiset.map (fun (i : ι) => f i a) s)) t

theorem continuous_finset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Finset ι) : (∀ i ∈ s, Continuous (f i)) → Continuous fun (a : X) => Finset.sum s fun (i : ι) => f i a

theorem continuous_finset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Finset ι) : (∀ i ∈ s, Continuous (f i)) → Continuous fun (a : X) => Finset.prod s fun (i : ι) => f i a

theorem continuousOn_finset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Finset ι) {t : Set X} : (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun (a : X) => Finset.sum s fun (i : ι) => f i a) t

theorem continuousOn_finset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Finset ι) {t : Set X} : (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun (a : X) => Finset.prod s fun (i : ι) => f i a) t

theorem eventuallyEq_sum {ι : Type u_1} {X : Type u_6} {M : Type u_7} [AddCommMonoid M] {s : Finset ι} {l : Filter X} {f : ι → X → M} {g : ι → X → M} (hs : ∀ i ∈ s, f i =ᶠ[l] g i) : (Finset.sum s fun (i : ι) => f i) =ᶠ[l] Finset.sum s fun (i : ι) => g i

theorem eventuallyEq_prod {ι : Type u_1} {X : Type u_6} {M : Type u_7} [CommMonoid M] {s : Finset ι} {l : Filter X} {f : ι → X → M} {g : ι → X → M} (hs : ∀ i ∈ s, f i =ᶠ[l] g i) : (Finset.prod s fun (i : ι) => f i) =ᶠ[l] Finset.prod s fun (i : ι) => g i

theorem LocallyFinite.exists_finset_support {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [AddCommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.support (f i)) (x₀ : X) : ∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x₀, (Function.support fun (i : ι) => f i x) ⊆ ↑I

theorem LocallyFinite.exists_finset_mulSupport {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [CommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (x₀ : X) : ∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x₀, (Function.mulSupport fun (i : ι) => f i x) ⊆ ↑I

abbrev finsum_eventually_eq_sum.match_1 {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {M : Type u_3} [AddCommMonoid M] {f : ι → X → M} (x : X) (motive : (∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) ⊆ ↑I) → Prop) : ∀ (x_1 : ∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) ⊆ ↑I), (∀ (I : Finset ι) (hI : ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) ⊆ ↑I), motive (_ : ∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) ⊆ ↑I)) → motive x_1

Equations

• (_ : motive x) = (_ : motive x)

theorem finsum_eventually_eq_sum {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [AddCommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.support (f i)) (x : X) : ∃ (s : Finset ι), ∀ᶠ (y : X) in nhds x, (finsum fun (i : ι) => f i y) = Finset.sum s fun (i : ι) => f i y

theorem finprod_eventually_eq_prod {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [CommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (x : X) : ∃ (s : Finset ι), ∀ᶠ (y : X) in nhds x, (finprod fun (i : ι) => f i y) = Finset.prod s fun (i : ι) => f i y

theorem continuous_finsum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (hc : ∀ (i : ι), Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.support (f i)) : Continuous fun (x : X) => finsum fun (i : ι) => f i x

theorem continuous_finprod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (hc : ∀ (i : ι), Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : Continuous fun (x : X) => finprod fun (i : ι) => f i x

theorem continuous_finsum_cond {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} {p : ι → Prop} (hc : ∀ (i : ι), p i → Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.support (f i)) : Continuous fun (x : X) => finsum fun (i : ι) => finsum fun (x_1 : p i) => f i x

theorem continuous_finprod_cond {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} {p : ι → Prop} (hc : ∀ (i : ι), p i → Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) : Continuous fun (x : X) => finprod fun (i : ι) => finprod fun (x_1 : p i) => f i x

instance instContinuousAddAdditiveInstTopologicalSpaceAdditiveAdd {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] : ContinuousAdd (Additive M)

Equations

• (_ : ContinuousAdd (Additive M)) = (_ : ContinuousAdd (Additive M))

instance instContinuousMulMultiplicativeInstTopologicalSpaceMultiplicativeMul {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] : ContinuousMul (Multiplicative M)

Equations

• (_ : ContinuousMul (Multiplicative M)) = (_ : ContinuousMul (Multiplicative M))

theorem continuousAdd_sInf {M : Type u_3} [Add M] {ts : Set (TopologicalSpace M)} (h : ∀ t ∈ ts, ContinuousAdd M) : ContinuousAdd M

theorem continuousMul_sInf {M : Type u_3} [Mul M] {ts : Set (TopologicalSpace M)} (h : ∀ t ∈ ts, ContinuousMul M) : ContinuousMul M

theorem continuousAdd_iInf {M : Type u_3} {ι' : Sort u_6} [Add M] {ts : ι' → TopologicalSpace M} (h' : ∀ (i : ι'), ContinuousAdd M) : ContinuousAdd M

theorem continuousMul_iInf {M : Type u_3} {ι' : Sort u_6} [Mul M] {ts : ι' → TopologicalSpace M} (h' : ∀ (i : ι'), ContinuousMul M) : ContinuousMul M

theorem continuousAdd_inf {M : Type u_3} [Add M] {t₁ : TopologicalSpace M} {t₂ : TopologicalSpace M} (h₁ : ContinuousAdd M) (h₂ : ContinuousAdd M) : ContinuousAdd M

theorem continuousMul_inf {M : Type u_3} [Mul M] {t₁ : TopologicalSpace M} {t₂ : TopologicalSpace M} (h₁ : ContinuousMul M) (h₂ : ContinuousMul M) : ContinuousMul M

def ContinuousMap.addRight {X : Type u_5} [TopologicalSpace X] [Add X] [ContinuousAdd X] (x : X) : C(X, X)

The continuous map fun y => y + x

Equations

• ContinuousMap.addRight x = ContinuousMap.mk fun (b : X) => b + x

def ContinuousMap.mulRight {X : Type u_5} [TopologicalSpace X] [Mul X] [ContinuousMul X] (x : X) : C(X, X)

The continuous map fun y => y * x

Equations

• ContinuousMap.mulRight x = ContinuousMap.mk fun (b : X) => b * x

@[simp]

theorem ContinuousMap.coe_addRight {X : Type u_5} [TopologicalSpace X] [Add X] [ContinuousAdd X] (x : X) : ⇑(ContinuousMap.addRight x) = fun (y : X) => y + x

@[simp]

theorem ContinuousMap.coe_mulRight {X : Type u_5} [TopologicalSpace X] [Mul X] [ContinuousMul X] (x : X) : ⇑(ContinuousMap.mulRight x) = fun (y : X) => y * x

def ContinuousMap.addLeft {X : Type u_5} [TopologicalSpace X] [Add X] [ContinuousAdd X] (x : X) : C(X, X)

The continuous map fun y => x + y

Equations

• ContinuousMap.addLeft x = ContinuousMap.mk fun (b : X) => x + b

def ContinuousMap.mulLeft {X : Type u_5} [TopologicalSpace X] [Mul X] [ContinuousMul X] (x : X) : C(X, X)

The continuous map fun y => x * y

Equations

• ContinuousMap.mulLeft x = ContinuousMap.mk fun (b : X) => x * b

@[simp]

theorem ContinuousMap.coe_addLeft {X : Type u_5} [TopologicalSpace X] [Add X] [ContinuousAdd X] (x : X) : ⇑(ContinuousMap.addLeft x) = fun (y : X) => x + y

@[simp]

theorem ContinuousMap.coe_mulLeft {X : Type u_5} [TopologicalSpace X] [Mul X] [ContinuousMul X] (x : X) : ⇑(ContinuousMap.mulLeft x) = fun (y : X) => x * y