# 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} [] [] [Zero M] :
theorem continuous_one {M : Type u_3} {X : Type u_5} [] [] [One M] :

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 αᵐᵒᵖ α.

Instances
Continuous fun (p : M × M) => p.1 + p.2
class ContinuousMul (M : Type u) [] [Mul M] :

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 αᵐᵒᵖ α.

Instances
theorem ContinuousMul.continuous_mul {M : Type u} [] [Mul M] [self : ] :
Continuous fun (p : M × M) => p.1 * p.2
Equations
• = inst
instance instContinuousMulOrderDual {M : Type u_3} [] [Mul M] [] :
Equations
• = inst
Continuous fun (p : M × M) => p.1 + p.2
theorem continuous_mul {M : Type u_3} [] [Mul M] [] :
Continuous fun (p : M × M) => p.1 * p.2
Equations
• =
instance instContinuousMulULift {M : Type u_3} [] [Mul M] [] :
Equations
• =
Equations
• =
instance ContinuousMul.to_continuousSMul {M : Type u_3} [] [Mul M] [] :
Equations
• =
Equations
• =
instance ContinuousMul.to_continuousSMul_op {M : Type u_3} [] [Mul M] [] :
Equations
• =
theorem Continuous.add {M : Type u_3} {X : Type u_5} [] [] [Add M] [] {f : XM} {g : XM} (hf : ) (hg : ) :
Continuous fun (x : X) => f x + g x
theorem Continuous.mul {M : Type u_3} {X : Type u_5} [] [] [Mul M] [] {f : XM} {g : XM} (hf : ) (hg : ) :
Continuous fun (x : X) => f x * g x
theorem continuous_add_left {M : Type u_3} [] [Add M] [] (a : M) :
Continuous fun (b : M) => a + b
theorem continuous_mul_left {M : Type u_3} [] [Mul M] [] (a : M) :
Continuous fun (b : M) => a * b
theorem continuous_add_right {M : Type u_3} [] [Add M] [] (a : M) :
Continuous fun (b : M) => b + a
theorem continuous_mul_right {M : Type u_3} [] [Mul M] [] (a : M) :
Continuous fun (b : M) => b * a
theorem ContinuousOn.add {M : Type u_3} {X : Type u_5} [] [] [Add M] [] {f : XM} {g : XM} {s : Set X} (hf : ) (hg : ) :
ContinuousOn (fun (x : X) => f x + g x) s
theorem ContinuousOn.mul {M : Type u_3} {X : Type u_5} [] [] [Mul M] [] {f : XM} {g : XM} {s : Set X} (hf : ) (hg : ) :
ContinuousOn (fun (x : X) => f x * g x) s
theorem tendsto_add {M : Type u_3} [] [Add 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} [] [Mul 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} [] [Add M] [] {f : αM} {g : αM} {x : } {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} [] [Mul M] [] {f : αM} {g : αM} {x : } {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} [] [Add M] [] (b : M) {c : M} {f : αM} {l : } (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} [] [Mul M] [] (b : M) {c : M} {f : αM} {l : } (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} [] [Add M] [] (b : M) {c : M} {f : αM} {l : } (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} [] [Mul M] [] (b : M) {c : M} {f : αM} {l : } (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} [] [Add M] [] (a : M) (b : M) :
nhds a + nhds b nhds (a + b)
theorem le_nhds_mul {M : Type u_3} [] [Mul M] [] (a : M) (b : M) :
nhds a * nhds b nhds (a * b)
@[simp]
theorem nhds_zero_add_nhds {M : Type u_6} [] [] [] (a : M) :
nhds 0 + nhds a = nhds a
@[simp]
theorem nhds_one_mul_nhds {M : Type u_6} [] [] [] (a : M) :
nhds 1 * nhds a = nhds a
@[simp]
theorem nhds_add_nhds_zero {M : Type u_6} [] [] [] (a : M) :
nhds a + nhds 0 = nhds a
@[simp]
theorem nhds_mul_nhds_one {M : Type u_6} [] [] [] (a : M) :
nhds a * nhds 1 = nhds a
theorem Filter.TendstoNhdsWithinIoi.const_mul {α : Type u_2} {𝕜 : Type u_6} [] [Zero 𝕜] [Mul 𝕜] [] [] {l : } {f : α𝕜} {b : 𝕜} {c : 𝕜} (hb : 0 < b) [] [] (h : Filter.Tendsto f l (nhdsWithin 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} [] [Zero 𝕜] [Mul 𝕜] [] [] {l : } {f : α𝕜} {b : 𝕜} {c : 𝕜} (hb : 0 < b) [] [] (h : Filter.Tendsto f l (nhdsWithin 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} [] [Zero 𝕜] [Mul 𝕜] [] [] {l : } {f : α𝕜} {b : 𝕜} {c : 𝕜} (hb : 0 < b) [] [] (h : Filter.Tendsto f l (nhdsWithin 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} [] [Zero 𝕜] [Mul 𝕜] [] [] {l : } {f : α𝕜} {b : 𝕜} {c : 𝕜} (hb : 0 < b) [] [] (h : Filter.Tendsto f l (nhdsWithin c ())) :
Filter.Tendsto (fun (a : α) => f a * b) l (nhdsWithin (c * b) (Set.Iio (c * b)))
theorem Specializes.add {M : Type u_3} [] [Add M] [] {a : M} {b : M} {c : M} {d : M} (hab : a b) (hcd : c d) :
(a + c) (b + d)
theorem Specializes.mul {M : Type u_3} [] [Mul M] [] {a : M} {b : M} {c : M} {d : M} (hab : a b) (hcd : c d) :
(a * c) (b * d)
theorem Inseparable.add {M : Type u_3} [] [Add M] [] {a : M} {b : M} {c : M} {d : M} (hab : ) (hcd : ) :
Inseparable (a + c) (b + d)
theorem Inseparable.mul {M : Type u_3} [] [Mul M] [] {a : M} {b : M} {c : M} {d : M} (hab : ) (hcd : ) :
Inseparable (a * c) (b * d)
theorem Specializes.nsmul {M : Type u_6} [] [] [] {a : M} {b : M} (h : a b) (n : ) :
(n a) (n b)
theorem Specializes.pow {M : Type u_6} [] [] [] {a : M} {b : M} (h : a b) (n : ) :
(a ^ n) (b ^ n)
theorem Inseparable.nsmul {M : Type u_6} [] [] [] {a : M} {b : M} (h : ) (n : ) :
Inseparable (n a) (n b)
theorem Inseparable.pow {M : Type u_6} [] [] [] {a : M} {b : M} (h : ) (n : ) :
Inseparable (a ^ n) (b ^ n)
theorem Filter.Tendsto.addUnits.proof_1 {ι : Type u_2} {N : Type u_1} [] [] [] [] {f : ι} {r₁ : N} {r₂ : N} {l : } [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (-f x)) l (nhds r₂)) :
r₁ + r₂ = 0
theorem Filter.Tendsto.addUnits.proof_2 {ι : Type u_2} {N : Type u_1} [] [] [] [] {f : ι} {r₁ : N} {r₂ : N} {l : } [l.NeBot] (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} [] [] [] [] {f : ι} {r₁ : N} {r₂ : N} {l : } [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (-f x)) l (nhds r₂)) :

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

Equations
• h₁.addUnits h₂ = { val := r₁, neg := r₂, val_neg := , neg_val := }
Instances For
@[simp]
theorem Filter.Tendsto.val_neg_addUnits {ι : Type u_1} {N : Type u_4} [] [] [] [] {f : ι} {r₁ : N} {r₂ : N} {l : } [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (-f x)) l (nhds r₂)) :
@[simp]
theorem Filter.Tendsto.val_units {ι : Type u_1} {N : Type u_4} [] [] [] [] {f : ιNˣ} {r₁ : N} {r₂ : N} {l : } [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (f x)⁻¹) l (nhds r₂)) :
(h₁.units h₂) = r₁
@[simp]
theorem Filter.Tendsto.val_inv_units {ι : Type u_1} {N : Type u_4} [] [] [] [] {f : ιNˣ} {r₁ : N} {r₂ : N} {l : } [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (f x)⁻¹) l (nhds r₂)) :
(h₁.units h₂)⁻¹ = r₂
@[simp]
theorem Filter.Tendsto.val_addUnits {ι : Type u_1} {N : Type u_4} [] [] [] [] {f : ι} {r₁ : N} {r₂ : N} {l : } [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (-f x)) l (nhds r₂)) :
def Filter.Tendsto.units {ι : Type u_1} {N : Type u_4} [] [] [] [] {f : ιNˣ} {r₁ : N} {r₂ : N} {l : } [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (f x)⁻¹) l (nhds r₂)) :

Construct a unit from limits of units and their inverses.

Equations
• h₁.units h₂ = { val := r₁, inv := r₂, val_inv := , inv_val := }
Instances For
theorem ContinuousAt.add {M : Type u_3} {X : Type u_5} [] [] [Add M] [] {f : XM} {g : XM} {x : X} (hf : ) (hg : ) :
ContinuousAt (fun (x : X) => f x + g x) x
theorem ContinuousAt.mul {M : Type u_3} {X : Type u_5} [] [] [Mul M] [] {f : XM} {g : XM} {x : X} (hf : ) (hg : ) :
ContinuousAt (fun (x : X) => f x * g x) x
theorem ContinuousWithinAt.add {M : Type u_3} {X : Type u_5} [] [] [Add M] [] {f : XM} {g : XM} {s : Set X} {x : X} (hf : ) (hg : ) :
ContinuousWithinAt (fun (x : X) => f x + g x) s x
theorem ContinuousWithinAt.mul {M : Type u_3} {X : Type u_5} [] [] [Mul M] [] {f : XM} {g : XM} {s : Set X} {x : X} (hf : ) (hg : ) :
ContinuousWithinAt (fun (x : X) => f x * g x) s x
instance Prod.continuousAdd {M : Type u_3} {N : Type u_4} [] [Add M] [] [] [Add N] [] :
Equations
• =
instance Prod.continuousMul {M : Type u_3} {N : Type u_4} [] [Mul M] [] [] [Mul N] [] :
Equations
• =
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
• =
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
• =
instance Pi.continuousAdd' {ι : Type u_1} {M : Type u_3} [] [Add 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
• =
instance Pi.continuousMul' {ι : Type u_1} {M : Type u_3} [] [Mul 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
• =
@[instance 100]
Equations
• =
@[instance 100]
instance continuousMul_of_discreteTopology {N : Type u_4} [] [Mul N] [] :
Equations
• =
theorem ContinuousAdd.of_nhds_zero {M : Type u} [] [] (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)) :
theorem ContinuousMul.of_nhds_one {M : Type u} [] [] (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)) :
theorem continuousAdd_of_comm_of_nhds_zero (M : Type u) [] [] (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)) :
theorem continuousMul_of_comm_of_nhds_one (M : Type u) [] [] (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)) :
theorem isClosed_setOf_map_zero (M₁ : Type u_6) (M₂ : Type u_7) [] [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) [] [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) [] [T2Space M₂] [Add M₁] [Add 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) [] [T2Space M₂] [Mul M₁] [Mul M₂] [] :
IsClosed {f : M₁M₂ | ∀ (x y : M₁), f (x * y) = f x * f y}
def addMonoidHomOfMemClosureRangeCoe {M₁ : Type u_6} {M₂ : Type u_7} [] [T2Space 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
• = { toFun := f, map_zero' := , map_add' := }
Instances For
theorem addMonoidHomOfMemClosureRangeCoe.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [] [T2Space 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}
theorem addMonoidHomOfMemClosureRangeCoe.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [] [T2Space 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' := }.toFun {f : M₁M₂ | ∀ (x y : M₁), f (x + y) = f x + f y}
@[simp]
theorem addMonoidHomOfMemClosureRangeCoe_apply {M₁ : Type u_6} {M₂ : Type u_7} [] [T2Space 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)) :
= f
@[simp]
theorem monoidHomOfMemClosureRangeCoe_apply {M₁ : Type u_6} {M₂ : Type u_7} [] [T2Space 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)) :
= f
def monoidHomOfMemClosureRangeCoe {M₁ : Type u_6} {M₂ : Type u_7} [] [T2Space 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
• = { toFun := f, map_one' := , map_mul' := }
Instances For
theorem addMonoidHomOfTendsto.proof_1 {α : Type u_4} {M₁ : Type u_1} {M₂ : Type u_2} [] {F : Type u_3} [FunLike F M₁ M₂] {l : } (f : M₁M₂) (g : αF) [l.NeBot] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :
f closure (Set.range fun (f : F) (x : M₁) => f x)
def addMonoidHomOfTendsto {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [] [T2Space M₂] [] [] [] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {l : } (f : M₁M₂) (g : αF) [l.NeBot] (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
Instances For
@[simp]
theorem addMonoidHomOfTendsto_apply {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [] [T2Space M₂] [] [] [] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {l : } (f : M₁M₂) (g : αF) [l.NeBot] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :
() = f
@[simp]
theorem monoidHomOfTendsto_apply {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [] [T2Space M₂] [] [] [] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {l : } (f : M₁M₂) (g : αF) [l.NeBot] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :
() = f
def monoidHomOfTendsto {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [] [T2Space M₂] [] [] [] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {l : } (f : M₁M₂) (g : αF) [l.NeBot] (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
Instances For
theorem AddMonoidHom.isClosed_range_coe (M₁ : Type u_6) (M₂ : Type u_7) [] [T2Space M₂] [] [] [] :
IsClosed (Set.range DFunLike.coe)
theorem MonoidHom.isClosed_range_coe (M₁ : Type u_6) (M₂ : Type u_7) [] [T2Space 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] [] [] [] (f : F) (hf : Inducing f) :
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] [] [] [] (f : F) (hf : Inducing f) :
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] [] [] (f : F) :
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] [] [] (f : F) :
instance AddSubsemigroup.continuousAdd {M : Type u_3} [] [] [] (S : ) :
Equations
• =
instance Subsemigroup.continuousMul {M : Type u_3} [] [] [] (S : ) :
Equations
• =
instance AddSubmonoid.continuousAdd {M : Type u_3} [] [] [] (S : ) :
Equations
• =
instance Submonoid.continuousMul {M : Type u_3} [] [] [] (S : ) :
Equations
• =
theorem exists_open_nhds_zero_half {M : Type u_3} [] [] [] {s : Set M} (hs : s nhds 0) :
∃ (V : Set M), 0 V vV, wV, v + w s
theorem exists_open_nhds_one_split {M : Type u_3} [] [] [] {s : Set M} (hs : s nhds 1) :
∃ (V : Set M), 1 V vV, wV, v * w s
abbrev exists_nhds_zero_half.match_1 {M : Type u_1} [] [] {s : Set M} (motive : (∃ (V : Set M), 0 V vV, wV, v + w s)Prop) :
∀ (x : ∃ (V : Set M), 0 V vV, wV, v + w s), (∀ (V : Set M) (Vo : ) (V1 : 0 V) (hV : vV, wV, v + w s), motive )motive x
Equations
• =
Instances For
theorem exists_nhds_zero_half {M : Type u_3} [] [] [] {s : Set M} (hs : s nhds 0) :
Vnhds 0, vV, wV, v + w s
theorem exists_nhds_one_split {M : Type u_3} [] [] [] {s : Set M} (hs : s nhds 1) :
Vnhds 1, vV, wV, v * w s
theorem exists_open_nhds_zero_add_subset {M : Type u_3} [] [] [] {U : Set M} (hU : U nhds 0) :
∃ (V : Set M), 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} [] [] [] {U : Set M} (hU : U nhds 1) :
∃ (V : Set M), 1 V V * V U

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

theorem AddSubmonoid.top_closure_add_self_subset {M : Type u_3} [] [] [] (s : ) :
closure s + closure s closure s
theorem Submonoid.top_closure_mul_self_subset {M : Type u_3} [] [] [] (s : ) :
closure s * closure s closure s
theorem AddSubmonoid.top_closure_add_self_eq {M : Type u_3} [] [] [] (s : ) :
closure s + closure s = closure s
theorem Submonoid.top_closure_mul_self_eq {M : Type u_3} [] [] [] (s : ) :
closure s * closure s = closure s
theorem AddSubmonoid.topologicalClosure.proof_1 {M : Type u_1} [] [] [] (s : ) :
∀ {a b : M}, a closure sb closure sa + b closure s
theorem AddSubmonoid.topologicalClosure.proof_2 {M : Type u_1} [] [] (s : ) :
0 closure s
def AddSubmonoid.topologicalClosure {M : Type u_3} [] [] [] (s : ) :

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

Equations
• s.topologicalClosure = { carrier := closure s, add_mem' := , zero_mem' := }
Instances For
def Submonoid.topologicalClosure {M : Type u_3} [] [] [] (s : ) :

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

Equations
• s.topologicalClosure = { carrier := closure s, mul_mem' := , one_mem' := }
Instances For
theorem AddSubmonoid.coe_topologicalClosure {M : Type u_3} [] [] [] (s : ) :
s.topologicalClosure = closure s
theorem Submonoid.coe_topologicalClosure {M : Type u_3} [] [] [] (s : ) :
s.topologicalClosure = closure s
theorem AddSubmonoid.le_topologicalClosure {M : Type u_3} [] [] [] (s : ) :
s s.topologicalClosure
theorem Submonoid.le_topologicalClosure {M : Type u_3} [] [] [] (s : ) :
s s.topologicalClosure
theorem AddSubmonoid.isClosed_topologicalClosure {M : Type u_3} [] [] [] (s : ) :
IsClosed s.topologicalClosure
theorem Submonoid.isClosed_topologicalClosure {M : Type u_3} [] [] [] (s : ) :
IsClosed s.topologicalClosure
theorem AddSubmonoid.topologicalClosure_minimal {M : Type u_3} [] [] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
theorem Submonoid.topologicalClosure_minimal {M : Type u_3} [] [] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
abbrev AddSubmonoid.addCommMonoidTopologicalClosure.match_1 {M : Type u_1} [] [] [] (s : ) (motive : s.topologicalClosureProp) :
∀ (x : s.topologicalClosure), (∀ (y : M) (hy : y s.topologicalClosure), motive y, hy)motive x
Equations
• =
Instances For
theorem AddSubmonoid.addCommMonoidTopologicalClosure.proof_1 {M : Type u_1} [] [] [] [] (s : ) (hs : ∀ (x y : s), x + y = y + x) :
∀ (x x_1 : s.topologicalClosure), x + x_1 = x_1 + x
def AddSubmonoid.addCommMonoidTopologicalClosure {M : Type u_3} [] [] [] [] (s : ) (hs : ∀ (x y : s), x + y = y + x) :

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

Equations
Instances For
def Submonoid.commMonoidTopologicalClosure {M : Type u_3} [] [] [] [] (s : ) (hs : ∀ (x y : s), x * y = y * x) :
CommMonoid s.topologicalClosure

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

Equations
• s.commMonoidTopologicalClosure hs = let __src := s.topologicalClosure.toMonoid;
Instances For
theorem exists_nhds_zero_quarter {M : Type u_3} [] [] [] {u : Set M} (hu : u nhds 0) :
Vnhds 0, ∀ {v w s t : M}, v Vw Vs Vt Vv + w + s + t u
theorem exists_nhds_one_split4 {M : Type u_3} [] [] [] {u : Set M} (hu : u nhds 1) :
Vnhds 1, ∀ {v w s t : M}, v Vw Vs Vt Vv * w * s * t u
theorem IsCompact.add {M : Type u_3} [] [] [] {s : Set M} {t : Set M} (hs : ) (ht : ) :
IsCompact (s + t)
theorem IsCompact.mul {M : Type u_3} [] [] [] {s : Set M} {t : Set M} (hs : ) (ht : ) :
IsCompact (s * t)
theorem tendsto_list_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [] [] [] {f : ιαM} {x : } {a : ιM} (l : List ι) :
(il, Filter.Tendsto (f i) x (nhds (a i)))Filter.Tendsto (fun (b : α) => (List.map (fun (c : ι) => f c b) l).sum) x (nhds (List.map a l).sum)
abbrev tendsto_list_sum.match_1 {ι : Type u_1} {α : Type u_2} {M : Type u_3} [] {f : ιαM} {x : } {a : ιM} (motive : (x_1 : List ι) → (ix_1, Filter.Tendsto (f i) x (nhds (a i)))Prop) :
∀ (x_1 : List ι) (x_2 : ix_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 : if_1 :: l, Filter.Tendsto (f i) x (nhds (a i))), motive (f_1 :: l) h)motive x_1 x_2
Equations
• =
Instances For
theorem tendsto_list_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [] [] [] {f : ιαM} {x : } {a : ιM} (l : List ι) :
(il, Filter.Tendsto (f i) x (nhds (a i)))Filter.Tendsto (fun (b : α) => (List.map (fun (c : ι) => f c b) l).prod) x (nhds (List.map a l).prod)
theorem continuous_list_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (l : List ι) (h : il, Continuous (f i)) :
Continuous fun (a : X) => (List.map (fun (i : ι) => f i a) l).sum
theorem continuous_list_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (l : List ι) (h : il, Continuous (f i)) :
Continuous fun (a : X) => (List.map (fun (i : ι) => f i a) l).prod
theorem continuousOn_list_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (l : List ι) {t : Set X} (h : il, ContinuousOn (f i) t) :
ContinuousOn (fun (a : X) => (List.map (fun (i : ι) => f i a) l).sum) t
theorem continuousOn_list_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (l : List ι) {t : Set X} (h : il, ContinuousOn (f i) t) :
ContinuousOn (fun (a : X) => (List.map (fun (i : ι) => f i a) l).prod) t
theorem continuous_nsmul {M : Type u_3} [] [] [] (n : ) :
Continuous fun (a : M) => n a
abbrev continuous_nsmul.match_1 (motive : ) :
∀ (x : ), (Unitmotive 0)(∀ (k : ), motive k.succ)motive x
Equations
• =
Instances For
theorem continuous_pow {M : Type u_3} [] [] [] (n : ) :
Continuous fun (a : M) => a ^ n
instance AddMonoid.continuousConstSMul_nat {A : Type u_6} [] [] [] :
Equations
• =
instance AddMonoid.continuousSMul_nat {A : Type u_6} [] [] [] :
Equations
• =
theorem Continuous.nsmul {M : Type u_3} {X : Type u_5} [] [] [] [] {f : XM} (h : ) (n : ) :
Continuous fun (b : X) => n f b
theorem Continuous.pow {M : Type u_3} {X : Type u_5} [] [] [] [] {f : XM} (h : ) (n : ) :
Continuous fun (b : X) => f b ^ n
theorem continuousOn_nsmul {M : Type u_3} [] [] [] {s : Set M} (n : ) :
ContinuousOn (fun (x : M) => n x) s
theorem continuousOn_pow {M : Type u_3} [] [] [] {s : Set M} (n : ) :
ContinuousOn (fun (x : M) => x ^ n) s
theorem continuousAt_nsmul {M : Type u_3} [] [] [] (x : M) (n : ) :
ContinuousAt (fun (x : M) => n x) x
theorem continuousAt_pow {M : Type u_3} [] [] [] (x : M) (n : ) :
ContinuousAt (fun (x : M) => x ^ n) x
theorem Filter.Tendsto.nsmul {α : Type u_2} {M : Type u_3} [] [] [] {l : } {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} [] [] [] {l : } {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} [] [] [] [] {f : XM} {x : X} {s : Set X} (hf : ) (n : ) :
ContinuousWithinAt (fun (x : X) => n f x) s x
theorem ContinuousWithinAt.pow {M : Type u_3} {X : Type u_5} [] [] [] [] {f : XM} {x : X} {s : Set X} (hf : ) (n : ) :
ContinuousWithinAt (fun (x : X) => f x ^ n) s x
theorem ContinuousAt.nsmul {M : Type u_3} {X : Type u_5} [] [] [] [] {f : XM} {x : X} (hf : ) (n : ) :
ContinuousAt (fun (x : X) => n f x) x
theorem ContinuousAt.pow {M : Type u_3} {X : Type u_5} [] [] [] [] {f : XM} {x : X} (hf : ) (n : ) :
ContinuousAt (fun (x : X) => f x ^ n) x
theorem ContinuousOn.nsmul {M : Type u_3} {X : Type u_5} [] [] [] [] {f : XM} {s : Set X} (hf : ) (n : ) :
ContinuousOn (fun (x : X) => n f x) s
theorem ContinuousOn.pow {M : Type u_3} {X : Type u_5} [] [] [] [] {f : XM} {s : Set X} (hf : ) (n : ) :
ContinuousOn (fun (x : X) => f x ^ n) s
theorem Filter.tendsto_cocompact_mul_left {M : Type u_3} [] [] [] {a : M} {b : M} (ha : b * a = 1) :
Filter.Tendsto (fun (x : M) => a * x) () ()

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} [] [] [] {a : M} {b : M} (ha : a * b = 1) :
Filter.Tendsto (fun (x : M) => x * a) () ()

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

@[instance 100]
instance VAddAssocClass.continuousConstVAdd {R : Type u_6} {A : Type u_7} [] [VAdd R A] [] [] [] :

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

Equations
• =
@[instance 100]
instance IsScalarTower.continuousConstSMul {R : Type u_6} {A : Type u_7} [] [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.

Equations
• =
@[instance 100]
instance VAddCommClass.continuousConstVAdd {R : Type u_6} {A : Type u_7} [] [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ᵃᵒᵖ.

Equations
• =
@[instance 100]
instance SMulCommClass.continuousConstSMul {R : Type u_6} {A : Type u_7} [] [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ᵐᵒᵖ.

Equations
• =

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

Equations
• =
instance MulOpposite.instContinuousMul {α : Type u_2} [] [Mul α] [] :

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

Equations
• =

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
• =
instance Units.instContinuousMul {α : Type u_2} [] [] [] :

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
• =
theorem Continuous.addUnits_map {M : Type u_3} {N : Type u_4} [] [] [] [] (f : M →+ N) (hf : ) :
theorem Continuous.units_map {M : Type u_3} {N : Type u_4} [] [] [] [] (f : M →* N) (hf : ) :
theorem AddSubmonoid.mem_nhds_zero {M : Type u_3} [] [] (S : ) (oS : IsOpen S) :
S nhds 0
theorem Submonoid.mem_nhds_one {M : Type u_3} [] [] (S : ) (oS : IsOpen S) :
S nhds 1
theorem tendsto_multiset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [] [] [] {f : ιαM} {x : } {a : ιM} (s : ) :
(is, Filter.Tendsto (f i) x (nhds (a i)))Filter.Tendsto (fun (b : α) => (Multiset.map (fun (c : ι) => f c b) s).sum) x (nhds ().sum)
theorem tendsto_multiset_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [] [] [] {f : ιαM} {x : } {a : ιM} (s : ) :
(is, Filter.Tendsto (f i) x (nhds (a i)))Filter.Tendsto (fun (b : α) => (Multiset.map (fun (c : ι) => f c b) s).prod) x (nhds ().prod)
theorem tendsto_finset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [] [] [] {f : ιαM} {x : } {a : ιM} (s : ) :
(is, Filter.Tendsto (f i) x (nhds (a i)))Filter.Tendsto (fun (b : α) => cs, f c b) x (nhds (cs, a c))
theorem tendsto_finset_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [] [] [] {f : ιαM} {x : } {a : ιM} (s : ) :
(is, Filter.Tendsto (f i) x (nhds (a i)))Filter.Tendsto (fun (b : α) => cs, f c b) x (nhds (cs, a c))
theorem continuous_multiset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (s : ) :
(is, Continuous (f i))Continuous fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).sum
theorem continuous_multiset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (s : ) :
(is, Continuous (f i))Continuous fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).prod
theorem continuousOn_multiset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (s : ) {t : Set X} :
(is, ContinuousOn (f i) t)ContinuousOn (fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).sum) t
theorem continuousOn_multiset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (s : ) {t : Set X} :
(is, ContinuousOn (f i) t)ContinuousOn (fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).prod) t
theorem continuous_finset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (s : ) :
(is, Continuous (f i))Continuous fun (a : X) => is, f i a
theorem continuous_finset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (s : ) :
(is, Continuous (f i))Continuous fun (a : X) => is, f i a
theorem continuousOn_finset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (s : ) {t : Set X} :
(is, ContinuousOn (f i) t)ContinuousOn (fun (a : X) => is, f i a) t
theorem continuousOn_finset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (s : ) {t : Set X} :
(is, ContinuousOn (f i) t)ContinuousOn (fun (a : X) => is, f i a) t
theorem eventuallyEq_sum {ι : Type u_1} {X : Type u_6} {M : Type u_7} [] {s : } {l : } {f : ιXM} {g : ιXM} (hs : is, f i =ᶠ[l] g i) :
is, f i =ᶠ[l] is, g i
theorem eventuallyEq_prod {ι : Type u_1} {X : Type u_6} {M : Type u_7} [] {s : } {l : } {f : ιXM} {g : ιXM} (hs : is, f i =ᶠ[l] g i) :
is, f i =ᶠ[l] is, g i
theorem LocallyFinite.exists_finset_support {ι : Type u_1} {X : Type u_5} [] {M : Type u_6} [] {f : ιXM} (hf : LocallyFinite fun (i : ι) => Function.support (f i)) (x₀ : X) :
∃ (I : ), ∀ᶠ (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} [] {M : Type u_6} [] {f : ιXM} (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (x₀ : X) :
∃ (I : ), ∀ᶠ (x : X) in nhds x₀, (Function.mulSupport fun (i : ι) => f i x) I
theorem finsum_eventually_eq_sum {ι : Type u_1} {X : Type u_5} [] {M : Type u_6} [] {f : ιXM} (hf : LocallyFinite fun (i : ι) => Function.support (f i)) (x : X) :
∃ (s : ), ∀ᶠ (y : X) in nhds x, ∑ᶠ (i : ι), f i y = is, f i y
abbrev finsum_eventually_eq_sum.match_1 {ι : Type u_1} {X : Type u_2} [] {M : Type u_3} [] {f : ιXM} (x : X) (motive : (∃ (I : ), ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) I)Prop) :
∀ (x_1 : ∃ (I : ), ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) I), (∀ (I : ) (hI : ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) I), motive )motive x_1
Equations
• =
Instances For
theorem finprod_eventually_eq_prod {ι : Type u_1} {X : Type u_5} [] {M : Type u_6} [] {f : ιXM} (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (x : X) :
∃ (s : ), ∀ᶠ (y : X) in nhds x, ∏ᶠ (i : ι), f i y = is, f i y
theorem continuous_finsum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (hc : ∀ (i : ι), Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.support (f i)) :
Continuous fun (x : X) => ∑ᶠ (i : ι), f i x
theorem continuous_finprod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} (hc : ∀ (i : ι), Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) :
Continuous fun (x : X) => ∏ᶠ (i : ι), f i x
theorem continuous_finsum_cond {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} {p : ιProp} (hc : ∀ (i : ι), p iContinuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.support (f i)) :
Continuous fun (x : X) => ∑ᶠ (i : ι) (_ : p i), f i x
theorem continuous_finprod_cond {ι : Type u_1} {M : Type u_3} {X : Type u_5} [] [] [] [] {f : ιXM} {p : ιProp} (hc : ∀ (i : ι), p iContinuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) :
Continuous fun (x : X) => ∏ᶠ (i : ι) (_ : p i), f i x
Equations
• =
Equations
• =
theorem continuousAdd_sInf {M : Type u_3} [Add M] {ts : } (h : tts, ) :
theorem continuousMul_sInf {M : Type u_3} [Mul M] {ts : } (h : tts, ) :
theorem continuousAdd_iInf {M : Type u_3} {ι' : Sort u_6} [Add M] {ts : ι'} (h' : ∀ (i : ι'), ) :
theorem continuousMul_iInf {M : Type u_3} {ι' : Sort u_6} [Mul M] {ts : ι'} (h' : ∀ (i : ι'), ) :
theorem continuousAdd_inf {M : Type u_3} [Add M] {t₁ : } {t₂ : } (h₁ : ) (h₂ : ) :
theorem continuousMul_inf {M : Type u_3} [Mul M] {t₁ : } {t₂ : } (h₁ : ) (h₂ : ) :
def ContinuousMap.addRight {X : Type u_5} [] [Add X] [] (x : X) :
C(X, X)

The continuous map fun y => y + x

Equations
• = { toFun := fun (b : X) => b + x, continuous_toFun := }
Instances For
def ContinuousMap.mulRight {X : Type u_5} [] [Mul X] [] (x : X) :
C(X, X)

The continuous map fun y => y * x

Equations
• = { toFun := fun (b : X) => b * x, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.coe_addRight {X : Type u_5} [] [Add X] [] (x : X) :
= fun (y : X) => y + x
@[simp]
theorem ContinuousMap.coe_mulRight {X : Type u_5} [] [Mul X] [] (x : X) :
= fun (y : X) => y * x
def ContinuousMap.addLeft {X : Type u_5} [] [Add X] [] (x : X) :
C(X, X)

The continuous map fun y => x + y

Equations
• = { toFun := fun (b : X) => x + b, continuous_toFun := }
Instances For
def ContinuousMap.mulLeft {X : Type u_5} [] [Mul X] [] (x : X) :
C(X, X)

The continuous map fun y => x * y

Equations
• = { toFun := fun (b : X) => x * b, continuous_toFun := }
Instances For
@[simp]
theorem ContinuousMap.coe_addLeft {X : Type u_5} [] [Add X] [] (x : X) :
= fun (y : X) => x + y
@[simp]
theorem ContinuousMap.coe_mulLeft {X : Type u_5} [] [Mul X] [] (x : X) :
= fun (y : X) => x * y