Documentation

Mathlib.Topology.Algebra.Monoid

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_one {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [One M] :
class ContinuousAdd (M : Type u) [TopologicalSpace M] [Add 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
    theorem ContinuousAdd.continuous_add {M : Type u} :
    ∀ {inst : TopologicalSpace M} {inst_1 : Add M} [self : ContinuousAdd M], Continuous fun (p : M × M) => p.1 + p.2
    class ContinuousMul (M : Type u) [TopologicalSpace M] [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} :
      ∀ {inst : TopologicalSpace M} {inst_1 : Mul M} [self : ContinuousMul M], Continuous fun (p : M × M) => p.1 * p.2
      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
      theorem ContinuousAdd.induced {α : Type u_6} {β : Type u_7} {F : Type u_8} [FunLike F α β] [AddZeroClass α] [AddZeroClass β] [AddMonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousAdd β] (f : F) :
      theorem ContinuousMul.induced {α : Type u_6} {β : Type u_7} {F : Type u_8} [FunLike F α β] [MulOneClass α] [MulOneClass β] [MonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousMul β] (f : F) :
      theorem Continuous.add {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Add M] [ContinuousAdd M] {f : XM} {g : XM} (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 : XM} {g : XM} (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 : XM} {g : XM} {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 : XM} {g : XM} {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 Specializes.add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd 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} [TopologicalSpace M] [Mul M] [ContinuousMul 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} [TopologicalSpace M] [Add M] [ContinuousAdd M] {a : M} {b : M} {c : M} {d : M} (hab : Inseparable a b) (hcd : Inseparable c d) :
      Inseparable (a + c) (b + d)
      theorem Inseparable.mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] {a : M} {b : M} {c : M} {d : M} (hab : Inseparable a b) (hcd : Inseparable c d) :
      Inseparable (a * c) (b * d)
      theorem Specializes.nsmul {M : Type u_6} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] {a : M} {b : M} (h : a b) (n : ) :
      (n a) (n b)
      theorem Specializes.pow {M : Type u_6} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a : M} {b : M} (h : a b) (n : ) :
      (a ^ n) (b ^ n)
      theorem Inseparable.nsmul {M : Type u_6} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] {a : M} {b : M} (h : Inseparable a b) (n : ) :
      Inseparable (n a) (n b)
      theorem Inseparable.pow {M : Type u_6} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a : M} {b : M} (h : Inseparable a b) (n : ) :
      Inseparable (a ^ n) (b ^ n)
      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 ι} [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_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 ι} [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} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ιAddUnits N} {r₁ : N} {r₂ : N} {l : Filter ι} [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_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 ι} [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} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ιAddUnits N} {r₁ : N} {r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (-f x)) l (nhds r₂)) :
        (h₁.addUnits 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 ι} [l.NeBot] (h₁ : Filter.Tendsto (fun (x : ι) => (f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun (x : ι) => (-f x)) l (nhds r₂)) :
        (-h₁.addUnits 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 ι} [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₁
        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 ι} [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} [TopologicalSpace X] [TopologicalSpace M] [Add M] [ContinuousAdd M] {f : XM} {g : XM} {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 : XM} {g : XM} {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 : XM} {g : XM} {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 : XM} {g : XM} {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] :
          Equations
          • =
          instance Prod.continuousMul {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [Mul M] [ContinuousMul M] [TopologicalSpace N] [Mul N] [ContinuousMul 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} [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
          • =
          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
          • =
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          theorem ContinuousAdd.of_nhds_zero {M : Type u} [AddMonoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : M) => x1 + x2) (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} [Monoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : M) => x1 * x2) (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) [AddCommMonoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : M) => x1 + x2) (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) [CommMonoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : M) => x1 * x2) (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) [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}
          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
          Instances For
            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}
            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' := }.toFun {f : M₁M₂ | ∀ (x y : M₁), f (x + y) = f x + f y}
            @[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)) :
            @[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)) :
            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
            Instances For
              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) [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} [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) [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} [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) [l.NeBot] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds 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) [l.NeBot] (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) [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) [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) :
                  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) :
                  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) :
                  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) :
                  Equations
                  • =
                  Equations
                  • =
                  Equations
                  • =
                  theorem exists_open_nhds_zero_half {M : Type u_3} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] {s : Set M} (hs : s nhds 0) :
                  ∃ (V : Set M), IsOpen V 0 V vV, wV, v + w s
                  theorem exists_open_nhds_one_split {M : Type u_3} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] {s : Set M} (hs : s nhds 1) :
                  ∃ (V : Set M), IsOpen V 1 V vV, wV, v * w s
                  theorem exists_nhds_zero_half {M : Type u_3} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] {s : Set M} (hs : s nhds 0) :
                  Vnhds 0, vV, wV, v + w s
                  theorem exists_nhds_one_split {M : Type u_3} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] {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} [TopologicalSpace M] [AddZeroClass 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] [MulOneClass 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 V * V ⊆ U.

                  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
                    theorem AddSubmonoid.topologicalClosure.proof_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :
                    ∀ {a b : M}, a closure sb closure sa + b closure 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} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :
                      s.topologicalClosure = closure s
                      theorem Submonoid.coe_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
                      s.topologicalClosure = closure s
                      theorem AddSubmonoid.le_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :
                      s s.topologicalClosure
                      theorem Submonoid.le_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
                      s s.topologicalClosure
                      theorem Submonoid.isClosed_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
                      IsClosed s.topologicalClosure
                      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) :
                      s.topologicalClosure 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) :
                      s.topologicalClosure 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 : s.topologicalClosure), 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 s.topologicalClosure

                      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} [TopologicalSpace M] [Monoid M] [ContinuousMul M] [T2Space M] (s : Submonoid M) (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
                        Instances For
                          theorem exists_nhds_zero_quarter {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {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} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {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} [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 ι) :
                          (∀ 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)
                          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 ι) :
                          (∀ 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} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {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} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {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} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {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} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {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} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (n : ) :
                          Continuous fun (a : M) => n a
                          theorem continuous_pow {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (n : ) :
                          Continuous fun (a : M) => a ^ n
                          theorem Continuous.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : XM} (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 : XM} (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 : XM} {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 : XM} {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 : XM} {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 : XM} {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 : XM} {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 : XM} {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 100]

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

                          Equations
                          • =
                          @[instance 100]

                          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]

                          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]

                          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
                          • =

                          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
                          • =

                          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} [AddMonoid M] [AddMonoid N] [TopologicalSpace M] [TopologicalSpace N] (f : M →+ N) (hf : Continuous 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) :
                          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 ι) :
                          (∀ is, Filter.Tendsto (f i) x (nhds (a i)))Filter.Tendsto (fun (b : α) => (Multiset.map (fun (c : ι) => f c b) s).sum) x (nhds (Multiset.map a s).sum)
                          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 ι) :
                          (∀ is, Filter.Tendsto (f i) x (nhds (a i)))Filter.Tendsto (fun (b : α) => (Multiset.map (fun (c : ι) => f c b) s).prod) x (nhds (Multiset.map a s).prod)
                          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 ι) :
                          (∀ 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} [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ιαM} {x : Filter α} {a : ιM} (s : Finset ι) :
                          (∀ 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} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ιXM} (s : Multiset ι) :
                          (∀ 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} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ιXM} (s : Multiset ι) :
                          (∀ 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} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ιXM} (s : Multiset ι) {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} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ιXM} (s : Multiset ι) {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} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ιXM} (s : Finset ι) :
                          (∀ 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} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ιXM} (s : Finset ι) :
                          (∀ 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} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ιXM} (s : Finset ι) {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} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ιXM} (s : Finset ι) {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} [AddCommMonoid M] {s : Finset ι} {l : Filter X} {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} [CommMonoid M] {s : Finset ι} {l : Filter X} {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} [TopologicalSpace X] {M : Type u_6} [AddCommMonoid M] {f : ιXM} (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 : ιXM} (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
                          theorem finsum_eventually_eq_sum {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [AddCommMonoid M] {f : ιXM} (hf : LocallyFinite fun (i : ι) => Function.support (f i)) (x : X) :
                          ∃ (s : Finset ι), ∀ᶠ (y : X) in nhds x, ∑ᶠ (i : ι), f i y = is, f i y
                          theorem finprod_eventually_eq_prod {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [CommMonoid M] {f : ιXM} (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (x : X) :
                          ∃ (s : Finset ι), ∀ᶠ (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} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {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} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {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} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {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} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {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
                          theorem continuousAdd_sInf {M : Type u_3} [Add M] {ts : Set (TopologicalSpace M)} (h : tts, ContinuousAdd M) :
                          theorem continuousMul_sInf {M : Type u_3} [Mul M] {ts : Set (TopologicalSpace M)} (h : tts, ContinuousMul M) :
                          theorem continuousAdd_iInf {M : Type u_3} {ι' : Sort u_6} [Add M] {ts : ι'TopologicalSpace M} (h' : ∀ (i : ι'), ContinuousAdd M) :
                          theorem continuousMul_iInf {M : Type u_3} {ι' : Sort u_6} [Mul M] {ts : ι'TopologicalSpace M} (h' : ∀ (i : ι'), ContinuousMul M) :
                          theorem continuousAdd_inf {M : Type u_3} [Add M] {t₁ : TopologicalSpace M} {t₂ : TopologicalSpace M} (h₁ : ContinuousAdd M) (h₂ : ContinuousAdd M) :
                          theorem continuousMul_inf {M : Type u_3} [Mul M] {t₁ : TopologicalSpace M} {t₂ : TopologicalSpace M} (h₁ : ContinuousMul M) (h₂ : 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
                          Instances For
                            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
                            Instances For
                              @[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
                              Instances For
                                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
                                Instances For
                                  @[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