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

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

      Equations
      Instances For
        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_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_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_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₁
        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₂)) :

        Construct a unit from limits of units and their inverses.

        Equations
        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
          • =
          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)) :
          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)) :
          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)) :
          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)) :
          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_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}
            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 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)) :
            @[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)) :
            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
              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
              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) [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 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
                @[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)) :
                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
                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
                  abbrev exists_nhds_zero_half.match_1 {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] {s : Set M} (motive : (∃ (V : Set M), IsOpen V 0 V vV, wV, v + w s)Prop) :
                  ∀ (x : ∃ (V : Set M), IsOpen V 0 V vV, wV, v + w s), (∀ (V : Set M) (Vo : IsOpen V) (V1 : 0 V) (hV : vV, wV, v + w s), motive )motive x
                  Equations
                  • =
                  Instances For
                    theorem exists_nhds_zero_half {M : Type u_3} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] {s : Set M} (hs : s nhds 0) :
                    ∃ V ∈ nhds 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) :
                    ∃ V ∈ nhds 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.

                    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 an additive submonoid of a space M with ContinuousAdd is itself an additive submonoid.

                    Equations
                    Instances For

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

                      Equations
                      Instances For
                        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
                        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
                        • =
                        Instances For

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

                            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) :
                              ∃ V ∈ nhds 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) :
                              ∃ V ∈ nhds 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.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 ι) → (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} [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.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 : ιXM} (l : List ι) (h : il, 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 : ιXM} (l : List ι) (h : il, 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 : ιXM} (l : List ι) {t : Set X} (h : il, 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 : ιXM} (l : List ι) {t : Set X} (h : il, 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 : ), (Unitmotive 0)(∀ (k : ), motive (Nat.succ k))motive x
                                Equations
                                • =
                                Instances For
                                  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.

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

                                  Equations
                                  • =

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

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

                                  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.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 ι) :
                                  (is, 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 ι) :
                                  (is, 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 ι) :
                                  (is, 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 : ιXM} (s : Multiset ι) :
                                  (is, 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 : ιXM} (s : Multiset ι) :
                                  (is, 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 : ιXM} (s : Multiset ι) {t : Set X} :
                                  (is, 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 : ιXM} (s : Multiset ι) {t : Set X} :
                                  (is, 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 : ιXM} (s : Finset ι) :
                                  (is, 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 : ιXM} (s : Finset ι) :
                                  (is, 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 : ιXM} (s : Finset ι) {t : Set X} :
                                  (is, 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 : ιXM} (s : Finset ι) {t : Set X} :
                                  (is, 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 : ιXM} {g : ιXM} (hs : is, 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 : ιXM} {g : ιXM} (hs : is, 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 : ι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, (finsum fun (i : ι) => f i y) = Finset.sum s fun (i : ι) => f i y
                                  abbrev finsum_eventually_eq_sum.match_1 {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {M : Type u_3} [AddCommMonoid M] {f : ιXM} (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 )motive x_1
                                  Equations
                                  • =
                                  Instances For
                                    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, (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 : ιXM} (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 : ιXM} (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 : ιXM} {p : ιProp} (hc : ∀ (i : ι), p iContinuous (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 : ιXM} {p : ιProp} (hc : ∀ (i : ι), p iContinuous (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
                                    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