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

source
theorem continuous_one {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [One M] :
Continuous 1
source
theorem continuous_zero {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Zero M] :
Continuous 0
source
instance instContinuousMulOrderDual {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] :
ContinuousMul M ᵒᵈ
source
instance instContinuousAddOrderDual {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] :
ContinuousAdd M ᵒᵈ
source
instance instContinuousMulULift {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] :
ContinuousMul (ULift.{u, u_3} M)
source
instance instContinuousAddULift {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] :
ContinuousAdd (ULift.{u, u_3} M)
source
instance ContinuousMul.to_continuousSMul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] :
ContinuousSMul M M
source
instance ContinuousAdd.to_continuousVAdd {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] :
ContinuousVAdd M M
source
instance ContinuousMul.to_continuousSMul_op {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] :
ContinuousSMul M ᵐᵒᵖ M
source
instance ContinuousAdd.to_continuousVAdd_op {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] :
ContinuousVAdd M ᵃᵒᵖ M
source
theorem ContinuousMul.induced {α : Type u_6} {β : Type u_7} {F : Type u_8} [FunLike F α β] [Mul α] [Mul β] [MulHomClass F α β] [tβ : TopologicalSpace β] [ContinuousMul β] (f : F) :
ContinuousMul α
source
theorem ContinuousAdd.induced {α : Type u_6} {β : Type u_7} {F : Type u_8} [FunLike F α β] [Add α] [Add β] [AddHomClass F α β] [tβ : TopologicalSpace β] [ContinuousAdd β] (f : F) :
ContinuousAdd α
source
theorem continuous_mul_left {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a : M) :
Continuous fun (b : M) => a * b
source
theorem continuous_add_left {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] (a : M) :
Continuous fun (b : M) => a + b
source
theorem continuous_mul_right {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a : M) :
Continuous fun (b : M) => b * a
source
theorem continuous_add_right {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] (a : M) :
Continuous fun (b : M) => b + a
source
theorem tendsto_mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] {a b : M} :
Filter.Tendsto (fun (p : M × M) => p.1 * p.2) (nhds (a, b)) (nhds (a * b))
source
theorem tendsto_add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] {a b : M} :
Filter.Tendsto (fun (p : M × M) => p.1 + p.2) (nhds (a, b)) (nhds (a + b))
source
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 : Tendsto (fun (k : α) => f k) l (nhds c)) :
Tendsto (fun (k : α) => b * f k) l (nhds (b * c))
source
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 : Tendsto (fun (k : α) => f k) l (nhds c)) :
Tendsto (fun (k : α) => b + f k) l (nhds (b + c))
source
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 : Tendsto (fun (k : α) => f k) l (nhds c)) :
Tendsto (fun (k : α) => f k * b) l (nhds (c * b))
source
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 : Tendsto (fun (k : α) => f k) l (nhds c)) :
Tendsto (fun (k : α) => f k + b) l (nhds (c + b))
source
theorem le_nhds_mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a b : M) :
nhds a * nhds b ≤ nhds (a * b)
source
theorem le_nhds_add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] (a b : M) :
nhds a + nhds b ≤ nhds (a + b)
source
@[simp]
theorem nhds_one_mul_nhds {M : Type u_6} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) :
nhds 1 * nhds a = nhds a
source
@[simp]
theorem nhds_zero_add_nhds {M : Type u_6} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] (a : M) :
nhds 0 + nhds a = nhds a
source
@[simp]
theorem nhds_mul_nhds_one {M : Type u_6} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) :
nhds a * nhds 1 = nhds a
source
@[simp]
theorem nhds_add_nhds_zero {M : Type u_6} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] (a : M) :
nhds a + nhds 0 = nhds a
source
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 𝕜] (h : Tendsto f l (nhdsWithin c (Set.Ioi c))) :
Tendsto (fun (a : α) => b * f a) l (nhdsWithin (b * c) (Set.Ioi (b * c)))
source
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 𝕜] (h : Tendsto f l (nhdsWithin c (Set.Iio c))) :
Tendsto (fun (a : α) => b * f a) l (nhdsWithin (b * c) (Set.Iio (b * c)))
source
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 𝕜] (h : Tendsto f l (nhdsWithin c (Set.Ioi c))) :
Tendsto (fun (a : α) => f a * b) l (nhdsWithin (c * b) (Set.Ioi (c * b)))
source
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 𝕜] (h : Tendsto f l (nhdsWithin c (Set.Iio c))) :
Tendsto (fun (a : α) => f a * b) l (nhdsWithin (c * b) (Set.Iio (c * b)))
source
theorem Specializes.mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] {a b c d : M} (hab : a ⤳ b) (hcd : c ⤳ d) :
(a * c) ⤳ (b * d)
source
theorem Specializes.add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] {a b c d : M} (hab : a ⤳ b) (hcd : c ⤳ d) :
(a + c) ⤳ (b + d)
source
theorem Inseparable.mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] {a b c d : M} (hab : Inseparable a b) (hcd : Inseparable c d) :
Inseparable (a * c) (b * d)
source
theorem Inseparable.add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] {a b c d : M} (hab : Inseparable a b) (hcd : Inseparable c d) :
Inseparable (a + c) (b + d)
source
theorem Specializes.pow {M : Type u_6} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a b : M} (h : a ⤳ b) (n : ℕ) :
(a ^ n) ⤳ (b ^ n)
source
theorem Specializes.nsmul {M : Type u_6} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] {a b : M} (h : a ⤳ b) (n : ℕ) :
(n • a) ⤳ (n • b)
source
theorem Inseparable.pow {M : Type u_6} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a b : M} (h : Inseparable a b) (n : ℕ) :
Inseparable (a ^ n) (b ^ n)
source
theorem Inseparable.nsmul {M : Type u_6} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] {a b : M} (h : Inseparable a b) (n : ℕ) :
Inseparable (n • a) (n • b)
source
def Filter.Tendsto.units {ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → N ˣ} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂)) :
N ˣ

Construct a unit from limits of units and their inverses.

Equations

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

Instances For

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

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

source
@[simp]
theorem Filter.Tendsto.val_units {ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → N ˣ} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂)) :
↑(h₁.units h₂) = r₁
source
@[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₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂)) :
↑(h₁.units h₂)⁻¹ = r₂
source
@[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₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂)) :
↑(h₁.addUnits h₂) = r₁
source
@[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₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁)) (h₂ : Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂)) :
↑(-h₁.addUnits h₂) = r₂
source
instance Prod.continuousMul {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [Mul M] [ContinuousMul M] [TopologicalSpace N] [Mul N] [ContinuousMul N] :
ContinuousMul (M × N)
source
instance Prod.continuousAdd {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [Add M] [ContinuousAdd M] [TopologicalSpace N] [Add N] [ContinuousAdd N] :
ContinuousAdd (M × N)
source
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)
source
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)
source
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.

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

source
@[instance 100]
instance continuousMul_of_discreteTopology {N : Type u_4} [TopologicalSpace N] [Mul N] [DiscreteTopology N] :
ContinuousMul N
source
@[instance 100]
instance continuousAdd_of_discreteTopology {N : Type u_4} [TopologicalSpace N] [Add N] [DiscreteTopology N] :
ContinuousAdd N
source
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)) :
ContinuousMul M
source
theorem ContinuousAdd.of_nhds_zero {M : Type u} [AddMonoid M] [TopologicalSpace M] (hadd : 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)) :
ContinuousAdd M
source
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)) :
ContinuousMul M
source
theorem continuousAdd_of_comm_of_nhds_zero (M : Type u) [AddCommMonoid M] [TopologicalSpace M] (hadd : 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)) :
ContinuousAdd M
source
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}
source
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}
source
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}
source
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}
source
def mulHomOfMemClosureRangeCoe {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Mul M₁] [Mul M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MulHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) :
M₁ →ₙ* M₂

Construct a bundled semigroup 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 `MulHomClass` instance) to `M₁ → M₂`.

Equations

- mulHomOfMemClosureRangeCoe f hf = { toFun := f, map_mul' := ⋯ }

Instances For

source
def addHomOfMemClosureRangeCoe {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Add M₁] [Add M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) :
M₁ →ₙ+ M₂

Construct a bundled additive semigroup 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 `AddHomClass` instance) to `M₁ → M₂`.

Equations

- addHomOfMemClosureRangeCoe f hf = { toFun := f, map_add' := ⋯ }

Instances For

source
@[simp]
theorem mulHomOfMemClosureRangeCoe_apply {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Mul M₁] [Mul M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MulHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) :
⇑(mulHomOfMemClosureRangeCoe f hf) = f
source
@[simp]
theorem addHomOfMemClosureRangeCoe_apply {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Add M₁] [Add M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) :
⇑(addHomOfMemClosureRangeCoe f hf) = f
source
def mulHomOfTendsto {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Mul M₁] [Mul M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MulHomClass 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 semigroup homomorphism from a pointwise limit of semigroup homomorphisms.

Equations

- mulHomOfTendsto f g h = mulHomOfMemClosureRangeCoe f ⋯

Instances For

source
def addHomOfTendsto {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Add M₁] [Add M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddHomClass 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 semigroup homomorphism from a pointwise limit of additive semigroup homomorphisms

Equations

- addHomOfTendsto f g h = addHomOfMemClosureRangeCoe f ⋯

Instances For

source
@[simp]
theorem mulHomOfTendsto_apply {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Mul M₁] [Mul M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MulHomClass 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)) :
⇑(mulHomOfTendsto f g h) = f
source
@[simp]
theorem addHomOfTendsto_apply {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Add M₁] [Add M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddHomClass 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)) :
⇑(addHomOfTendsto f g h) = f
source
theorem MulHom.isClosed_range_coe (M₁ : Type u_6) (M₂ : Type u_7) [TopologicalSpace M₂] [T2Space M₂] [Mul M₁] [Mul M₂] [ContinuousMul M₂] :
IsClosed (Set.range DFunLike.coe)
source
theorem AddHom.isClosed_range_coe (M₁ : Type u_6) (M₂ : Type u_7) [TopologicalSpace M₂] [T2Space M₂] [Add M₁] [Add M₂] [ContinuousAdd M₂] :
IsClosed (Set.range DFunLike.coe)
source
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

- monoidHomOfMemClosureRangeCoe f hf = { toFun := f, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
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

- addMonoidHomOfMemClosureRangeCoe f hf = { toFun := f, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem addMonoidHomOfMemClosureRangeCoe_apply {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) :
⇑(addMonoidHomOfMemClosureRangeCoe f hf) = f
source
@[simp]
theorem monoidHomOfMemClosureRangeCoe_apply {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [MulOneClass M₁] [MulOneClass M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun (f : F) (x : M₁) => f x)) :
⇑(monoidHomOfMemClosureRangeCoe f hf) = f
source
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

- monoidHomOfTendsto f g h = monoidHomOfMemClosureRangeCoe f ⋯

Instances For

source
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

- addMonoidHomOfTendsto f g h = addMonoidHomOfMemClosureRangeCoe f ⋯

Instances For

source
@[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
source
@[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)) :
⇑(addMonoidHomOfTendsto f g h) = f
source
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)
source
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)
source
theorem Topology.IsInducing.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 : IsInducing ⇑f) :
ContinuousMul M
source
theorem Topology.IsInducing.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 : IsInducing ⇑f) :
ContinuousAdd M
source
theorem continuousMul_induced {M : Type u_6} {N : Type u_7} {F : Type u_8} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [TopologicalSpace N] [ContinuousMul N] (f : F) :
ContinuousMul M
source
theorem continuousAdd_induced {M : Type u_6} {N : Type u_7} {F : Type u_8} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] [TopologicalSpace N] [ContinuousAdd N] (f : F) :
ContinuousAdd M
source
instance Subsemigroup.continuousMul {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] (S : Subsemigroup M) :
ContinuousMul ↥S
source
instance AddSubsemigroup.continuousAdd {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (S : AddSubsemigroup M) :
ContinuousAdd ↥S
source
instance Submonoid.continuousMul {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (S : Submonoid M) :
ContinuousMul ↥S
source
instance AddSubmonoid.continuousAdd {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (S : AddSubmonoid M) :
ContinuousAdd ↥S
source
theorem exists_mem_nhds_zero_mul_subset {M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {K U : Set M} (hK : IsCompact K) (hU : U ∈ nhds 0) :
∃ V ∈ nhds 0, K * V ⊆ U
source
theorem tendsto_mul_nhds_zero_prod_of_disjoint_cocompact {M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {l : Filter M} (hl : Disjoint l (Filter.cocompact M)) :
Filter.Tendsto (fun (x : M × M) => x.1 * x.2) (nhds 0 ×ˢ l) (nhds 0)

Let `M` be a topological space with a continuous multiplication operation and a `0`. Let `l` be a filter on `M` which is disjoint from the cocompact filter. Then, the multiplication map `M × M → M` tends to zero on the filter product `𝓝 0 ×ˢ l`.

source
theorem tendsto_mul_prod_nhds_zero_of_disjoint_cocompact {M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {l : Filter M} (hl : Disjoint l (Filter.cocompact M)) :
Filter.Tendsto (fun (x : M × M) => x.1 * x.2) (l ×ˢ nhds 0) (nhds 0)

Let `M` be a topological space with a continuous multiplication operation and a `0`. Let `l` be a filter on `M` which is disjoint from the cocompact filter. Then, the multiplication map `M × M → M` tends to zero on the filter product `l ×ˢ 𝓝 0`.

source
theorem tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact {M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {l : Filter (M × M)} (hl : Disjoint l (Filter.cocompact (M × M))) :
Filter.Tendsto (fun (x : M × M) => x.1 * x.2) ((nhds 0).coprod (nhds 0) ⊓ l) (nhds 0)

Let `M` be a topological space with a continuous multiplication operation and a `0`. Let `l` be a filter on `M × M` which is disjoint from the cocompact filter. Then, the multiplication map `M × M → M` tends to zero on `(𝓝 0).coprod (𝓝 0) ⊓ l`.

source
theorem tendsto_mul_nhds_zero_of_disjoint_cocompact {M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {l : Filter (M × M)} (hl : Disjoint l (Filter.cocompact (M × M))) (h'l : l ≤ (nhds 0).coprod (nhds 0)) :
Filter.Tendsto (fun (x : M × M) => x.1 * x.2) l (nhds 0)

Let `M` be a topological space with a continuous multiplication operation and a `0`. Let `l` be a filter on `M × M` which is both disjoint from the cocompact filter and less than or equal to `(𝓝 0).coprod (𝓝 0)`. Then the multiplication map `M × M → M` tends to zero on `l`.

source
theorem Tendsto.tendsto_mul_zero_of_disjoint_cocompact_right {M : Type u_3} {α : Type u_6} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {f g : α → M} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Disjoint (Filter.map g l) (Filter.cocompact M)) :
Filter.Tendsto (fun (x : α) => f x * g x) l (nhds 0)

Let `M` be a topological space with a continuous multiplication operation and a `0`. Let `f : α → M` and `g : α → M` be functions. If `f` tends to zero on a filter `l` and the image of `l` under `g` is disjoint from the cocompact filter on `M`, then `fun x : α ↦ f x * g x` also tends to zero on `l`.

source
theorem Tendsto.tendsto_mul_zero_of_disjoint_cocompact_left {M : Type u_3} {α : Type u_6} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {f g : α → M} {l : Filter α} (hf : Disjoint (Filter.map f l) (Filter.cocompact M)) (hg : Filter.Tendsto g l (nhds 0)) :
Filter.Tendsto (fun (x : α) => f x * g x) l (nhds 0)

Let `M` be a topological space with a continuous multiplication operation and a `0`. Let `f : α → M` and `g : α → M` be functions. If `g` tends to zero on a filter `l` and the image of `l` under `f` is disjoint from the cocompact filter on `M`, then `fun x : α ↦ f x * g x` also tends to zero on `l`.

source
theorem tendsto_mul_cocompact_nhds_zero {M : Type u_3} {α : Type u_6} {β : Type u_7} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] [TopologicalSpace α] [TopologicalSpace β] {f : α → M} {g : β → M} (f_cont : Continuous f) (g_cont : Continuous g) (hf : Filter.Tendsto f (Filter.cocompact α) (nhds 0)) (hg : Filter.Tendsto g (Filter.cocompact β) (nhds 0)) :
Filter.Tendsto (fun (i : α × β) => f i.1 * g i.2) (Filter.cocompact (α × β)) (nhds 0)

If `f : α → M` and `g : β → M` are continuous and both tend to zero on the cocompact filter, then `fun i : α × β ↦ f i.1 * g i.2` also tends to zero on the cocompact filter.

source
theorem tendsto_mul_cofinite_nhds_zero {M : Type u_3} {α : Type u_6} {β : Type u_7} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {f : α → M} {g : β → M} (hf : Filter.Tendsto f Filter.cofinite (nhds 0)) (hg : Filter.Tendsto g Filter.cofinite (nhds 0)) :
Filter.Tendsto (fun (i : α × β) => f i.1 * g i.2) Filter.cofinite (nhds 0)

If `f : α → M` and `g : β → M` both tend to zero on the cofinite filter, then so does `fun i : α × β ↦ f i.1 * g i.2`.

source
theorem GroupWithZero.isOpen_singleton_zero {M : Type u_3} [GroupWithZero M] [TopologicalSpace M] [ContinuousMul M] [CompactSpace M] [T1Space M] :
IsOpen {0}
source
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 ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
source
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 ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s
source
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, ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
source
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, ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s
source
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`.

source
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`.

source
theorem Filter.HasBasis.mul_self {ι : Type u_1} {M : Type u_3} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] {p : ι → Prop} {s : ι → Set M} (h : (nhds 1).HasBasis p s) :
(nhds 1).HasBasis p fun (i : ι) => s i * s i
source
theorem Filter.HasBasis.add_self {ι : Type u_1} {M : Type u_3} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] {p : ι → Prop} {s : ι → Set M} (h : (nhds 0).HasBasis p s) :
(nhds 0).HasBasis p fun (i : ι) => s i + s i
source
theorem Subsemigroup.top_closure_mul_self_subset {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] (s : Subsemigroup M) :
_root_.closure ↑s * _root_.closure ↑s ⊆ _root_.closure ↑s
source
theorem AddSubsemigroup.top_closure_add_self_subset {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (s : AddSubsemigroup M) :
_root_.closure ↑s + _root_.closure ↑s ⊆ _root_.closure ↑s
source
def Subsemigroup.topologicalClosure {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] (s : Subsemigroup M) :
Subsemigroup M

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

Equations

- s.topologicalClosure = { carrier := closure ↑s, mul_mem' := ⋯ }

Instances For

source
def AddSubsemigroup.topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (s : AddSubsemigroup M) :
AddSubsemigroup M

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' := ⋯ }

Instances For

source
theorem Subsemigroup.coe_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] (s : Subsemigroup M) :
↑s.topologicalClosure = _root_.closure ↑s
source
theorem AddSubsemigroup.coe_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (s : AddSubsemigroup M) :
↑s.topologicalClosure = _root_.closure ↑s
source
theorem Subsemigroup.le_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] (s : Subsemigroup M) :
s ≤ s.topologicalClosure
source
theorem AddSubsemigroup.le_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (s : AddSubsemigroup M) :
s ≤ s.topologicalClosure
source
theorem Subsemigroup.isClosed_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] (s : Subsemigroup M) :
IsClosed ↑s.topologicalClosure
source
theorem AddSubsemigroup.isClosed_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (s : AddSubsemigroup M) :
IsClosed ↑s.topologicalClosure
source
theorem Subsemigroup.topologicalClosure_minimal {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] (s : Subsemigroup M) {t : Subsemigroup M} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
theorem AddSubsemigroup.topologicalClosure_minimal {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (s : AddSubsemigroup M) {t : AddSubsemigroup M} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
@[reducible, inline]
abbrev Subsemigroup.commSemigroupTopologicalClosure {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] [T2Space M] (s : Subsemigroup M) (hs : ∀ (x y : ↥s), x * y = y * x) :
CommSemigroup ↥s.topologicalClosure

If a subsemigroup of a topological semigroup is commutative, then so is its topological closure.

See note [reducible non-instances]

Equations

- s.commSemigroupTopologicalClosure hs = { toSemigroup := MulMemClass.toSemigroup s.topologicalClosure, mul_comm := ⋯ }

Instances For

source
@[reducible, inline]
abbrev AddSubsemigroup.addCommSemigroupTopologicalClosure {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] [T2Space M] (s : AddSubsemigroup M) (hs : ∀ (x y : ↥s), x + y = y + x) :
AddCommSemigroup ↥s.topologicalClosure

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

See note [reducible non-instances]

Equations

- s.addCommSemigroupTopologicalClosure hs = { toAddSemigroup := AddMemClass.toAddSemigroup s.topologicalClosure, add_comm := ⋯ }

Instances For

source
theorem IsCompact.mul {M : Type u_3} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] {s t : Set M} (hs : IsCompact s) (ht : IsCompact t) :
IsCompact (s * t)
source
theorem IsCompact.add {M : Type u_3} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] {s t : Set M} (hs : IsCompact s) (ht : IsCompact t) :
IsCompact (s + t)
source
theorem Submonoid.top_closure_mul_self_subset {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
_root_.closure ↑s * _root_.closure ↑s ⊆ _root_.closure ↑s
source
theorem AddSubmonoid.top_closure_add_self_subset {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :
_root_.closure ↑s + _root_.closure ↑s ⊆ _root_.closure ↑s
source
theorem Submonoid.top_closure_mul_self_eq {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
_root_.closure ↑s * _root_.closure ↑s = _root_.closure ↑s
source
theorem AddSubmonoid.top_closure_add_self_eq {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :
_root_.closure ↑s + _root_.closure ↑s = _root_.closure ↑s
source
def Submonoid.topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
Submonoid M

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

Equations

- s.topologicalClosure = { carrier := closure ↑s, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

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

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

Equations

- s.topologicalClosure = { carrier := closure ↑s, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source
theorem Submonoid.coe_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
↑s.topologicalClosure = _root_.closure ↑s
source
theorem AddSubmonoid.coe_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :
↑s.topologicalClosure = _root_.closure ↑s
source
theorem Submonoid.le_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
s ≤ s.topologicalClosure
source
theorem AddSubmonoid.le_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :
s ≤ s.topologicalClosure
source
theorem Submonoid.isClosed_topologicalClosure {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (s : Submonoid M) :
IsClosed ↑s.topologicalClosure
source
theorem AddSubmonoid.isClosed_topologicalClosure {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :
IsClosed ↑s.topologicalClosure
source
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
source
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
source
@[reducible, inline]
abbrev 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

- s.commMonoidTopologicalClosure hs = { toMonoid := s.topologicalClosure.toMonoid, mul_comm := ⋯ }

Instances For

source
@[reducible, inline]
abbrev 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.

See note [reducible non-instances].

Equations

- s.addCommMonoidTopologicalClosure hs = { toAddMonoid := s.topologicalClosure.toAddMonoid, add_comm := ⋯ }

Instances For

source
theorem exists_nhds_one_split4 {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {u : Set M} (hu : u ∈ nhds 1) :
∃ V ∈ nhds 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
source
theorem exists_nhds_zero_quarter {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {u : Set M} (hu : u ∈ nhds 0) :
∃ V ∈ nhds 0, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v + w + s + t ∈ u
source
theorem tendsto_list_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι) :
(∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => (List.map (fun (c : ι) => f c b) l).prod) x (nhds (List.map a l).prod)
source
theorem tendsto_list_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι) :
(∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => (List.map (fun (c : ι) => f c b) l).sum) x (nhds (List.map a l).sum)
source
theorem continuous_list_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : ι → X → M} (l : List ι) (h : ∀ i ∈ l, Continuous (f i)) :
Continuous fun (a : X) => (List.map (fun (i : ι) => f i a) l).prod
source
theorem continuous_list_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : ι → X → M} (l : List ι) (h : ∀ i ∈ l, Continuous (f i)) :
Continuous fun (a : X) => (List.map (fun (i : ι) => f i a) l).sum
source
theorem continuousOn_list_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : ι → X → M} (l : List ι) {t : Set X} (h : ∀ i ∈ l, ContinuousOn (f i) t) :
ContinuousOn (fun (a : X) => (List.map (fun (i : ι) => f i a) l).prod) t
source
theorem continuousOn_list_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : ι → X → M} (l : List ι) {t : Set X} (h : ∀ i ∈ l, ContinuousOn (f i) t) :
ContinuousOn (fun (a : X) => (List.map (fun (i : ι) => f i a) l).sum) t
source
theorem continuous_pow {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (n : ℕ) :
Continuous fun (a : M) => a ^ n
source
theorem continuous_nsmul {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (n : ℕ) :
Continuous fun (a : M) => n • a
source
instance AddMonoid.continuousConstSMul_nat {A : Type u_6} [AddMonoid A] [TopologicalSpace A] [ContinuousAdd A] :
ContinuousConstSMul ℕ A
source
instance AddMonoid.continuousSMul_nat {A : Type u_6} [AddMonoid A] [TopologicalSpace A] [ContinuousAdd A] :
ContinuousSMul ℕ A
source
theorem Continuous.pow {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : X → M} (h : Continuous f) (n : ℕ) :
Continuous fun (b : X) => f b ^ n
source
theorem Continuous.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : X → M} (h : Continuous f) (n : ℕ) :
Continuous fun (b : X) => n • f b
source
theorem continuousOn_pow {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {s : Set M} (n : ℕ) :
ContinuousOn (fun (x : M) => x ^ n) s
source
theorem continuousOn_nsmul {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {s : Set M} (n : ℕ) :
ContinuousOn (fun (x : M) => n • x) s
source
theorem continuousAt_pow {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (x : M) (n : ℕ) :
ContinuousAt (fun (x : M) => x ^ n) x
source
theorem continuousAt_nsmul {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (x : M) (n : ℕ) :
ContinuousAt (fun (x : M) => n • x) x
source
theorem Filter.Tendsto.pow {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {l : Filter α} {f : α → M} {x : M} (hf : Tendsto f l (nhds x)) (n : ℕ) :
Tendsto (fun (x : α) => f x ^ n) l (nhds (x ^ n))
source
theorem Filter.Tendsto.nsmul {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {l : Filter α} {f : α → M} {x : M} (hf : Tendsto f l (nhds x)) (n : ℕ) :
Tendsto (fun (x : α) => n • f x) l (nhds (n • x))
source
theorem ContinuousWithinAt.pow {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : X → M} {x : X} {s : Set X} (hf : ContinuousWithinAt f s x) (n : ℕ) :
ContinuousWithinAt (fun (x : X) => f x ^ n) s x
source
theorem ContinuousWithinAt.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : X → M} {x : X} {s : Set X} (hf : ContinuousWithinAt f s x) (n : ℕ) :
ContinuousWithinAt (fun (x : X) => n • f x) s x
source
theorem ContinuousAt.pow {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : X → M} {x : X} (hf : ContinuousAt f x) (n : ℕ) :
ContinuousAt (fun (x : X) => f x ^ n) x
source
theorem ContinuousAt.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : X → M} {x : X} (hf : ContinuousAt f x) (n : ℕ) :
ContinuousAt (fun (x : X) => n • f x) x
source
theorem ContinuousOn.pow {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : X → M} {s : Set X} (hf : ContinuousOn f s) (n : ℕ) :
ContinuousOn (fun (x : X) => f x ^ n) s
source
theorem ContinuousOn.nsmul {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : X → M} {s : Set X} (hf : ContinuousOn f s) (n : ℕ) :
ContinuousOn (fun (x : X) => n • f x) s
source
theorem Filter.tendsto_cocompact_mul_left {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {a b : M} (ha : b * a = 1) :
Tendsto (fun (x : M) => a * x) (cocompact M) (cocompact M)

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

source
theorem Filter.tendsto_cocompact_mul_right {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {a b : M} (ha : a * b = 1) :
Tendsto (fun (x : M) => x * a) (cocompact M) (cocompact M)

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

source
@[instance 100]
instance IsScalarTower.continuousConstSMul {R : Type u_6} {A : Type u_7} [Monoid A] [SMul R A] [IsScalarTower R A A] [TopologicalSpace A] [ContinuousMul A] :
ContinuousConstSMul R A

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

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

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

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

source
@[instance 100]
instance SMulCommClass.continuousConstSMul {R : Type u_6} {A : Type u_7} [Monoid A] [SMul R A] [SMulCommClass R A A] [TopologicalSpace A] [ContinuousMul A] :
ContinuousConstSMul R A

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

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

source
@[instance 100]
instance VAddCommClass.continuousConstVAdd {R : Type u_6} {A : Type u_7} [AddMonoid A] [VAdd R A] [VAddCommClass R A A] [TopologicalSpace A] [ContinuousAdd A] :
ContinuousConstVAdd R A

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

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

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

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

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

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

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

If multiplication on a monoid is continuous, then multiplication on the units of the monoid, with respect to the induced topology, is continuous.

Inversion is also continuous, but we register this in a later file, `Topology.Algebra.Group`, because the predicate `ContinuousInv` has not yet been defined.

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

If addition on an additive monoid is continuous, then addition on the additive units of the monoid, with respect to the induced topology, is continuous.

Negation is also continuous, but we register this in a later file, `Topology.Algebra.Group`, because the predicate `ContinuousNeg` has not yet been defined.

source
theorem Continuous.units_map {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N] (f : M →* N) (hf : Continuous ⇑f) :
Continuous ⇑(Units.map f)
source
theorem Continuous.addUnits_map {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] [TopologicalSpace M] [TopologicalSpace N] (f : M →+ N) (hf : Continuous ⇑f) :
Continuous ⇑(AddUnits.map f)
source
theorem Submonoid.mem_nhds_one {M : Type u_3} [TopologicalSpace M] [CommMonoid M] (S : Submonoid M) (oS : IsOpen ↑S) :
↑S ∈ nhds 1
source
theorem AddSubmonoid.mem_nhds_zero {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] (S : AddSubmonoid M) (oS : IsOpen ↑S) :
↑S ∈ nhds 0
source
theorem tendsto_multiset_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) :
(∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => (Multiset.map (fun (c : ι) => f c b) s).prod) x (nhds (Multiset.map a s).prod)
source
theorem tendsto_multiset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) :
(∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => (Multiset.map (fun (c : ι) => f c b) s).sum) x (nhds (Multiset.map a s).sum)
source
theorem tendsto_finset_prod {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) :
(∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => ∏ c ∈ s, f c b) x (nhds (∏ c ∈ s, a c))
source
theorem tendsto_finset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) :
(∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => ∑ c ∈ s, f c b) x (nhds (∑ c ∈ s, a c))
source
theorem continuous_multiset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Multiset ι) :
(∀ i ∈ s, Continuous (f i)) → Continuous fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).prod
source
theorem continuous_multiset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Multiset ι) :
(∀ i ∈ s, Continuous (f i)) → Continuous fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).sum
source
theorem continuousOn_multiset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Multiset ι) {t : Set X} :
(∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).prod) t
source
theorem continuousOn_multiset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Multiset ι) {t : Set X} :
(∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).sum) t
source
theorem continuous_finset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Finset ι) :
(∀ i ∈ s, Continuous (f i)) → Continuous fun (a : X) => ∏ i ∈ s, f i a
source
theorem continuous_finset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Finset ι) :
(∀ i ∈ s, Continuous (f i)) → Continuous fun (a : X) => ∑ i ∈ s, f i a
source
theorem continuousOn_finset_prod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Finset ι) {t : Set X} :
(∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun (a : X) => ∏ i ∈ s, f i a) t
source
theorem continuousOn_finset_sum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Finset ι) {t : Set X} :
(∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun (a : X) => ∑ i ∈ s, f i a) t
source
theorem eventuallyEq_prod {ι : Type u_1} {X : Type u_6} {M : Type u_7} [CommMonoid M] {s : Finset ι} {l : Filter X} {f g : ι → X → M} (hs : ∀ i ∈ s, f i =ᶠ[l] g i) :
∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i
source
theorem eventuallyEq_sum {ι : Type u_1} {X : Type u_6} {M : Type u_7} [AddCommMonoid M] {s : Finset ι} {l : Filter X} {f g : ι → X → M} (hs : ∀ i ∈ s, f i =ᶠ[l] g i) :
∑ i ∈ s, f i =ᶠ[l] ∑ i ∈ s, g i
source
theorem LocallyFinite.exists_finset_mulSupport {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [One M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (x₀ : X) :
∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x₀, (Function.mulSupport fun (i : ι) => f i x) ⊆ ↑I
source
theorem LocallyFinite.exists_finset_support {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [Zero M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.support (f i)) (x₀ : X) :
∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x₀, (Function.support fun (i : ι) => f i x) ⊆ ↑I
source
theorem finprod_eventually_eq_prod {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [CommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (x : X) :
∃ (s : Finset ι), ∀ᶠ (y : X) in nhds x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y
source
theorem finsum_eventually_eq_sum {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [AddCommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.support (f i)) (x : X) :
∃ (s : Finset ι), ∀ᶠ (y : X) in nhds x, ∑ᶠ (i : ι), f i y = ∑ i ∈ s, f i y
source
theorem continuous_finprod {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} (hc : ∀ (i : ι), Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) :
Continuous fun (x : X) => ∏ᶠ (i : ι), f i x
source
theorem continuous_finsum {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (hc : ∀ (i : ι), Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.support (f i)) :
Continuous fun (x : X) => ∑ᶠ (i : ι), f i x
source
theorem continuous_finprod_cond {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → X → M} {p : ι → Prop} (hc : ∀ (i : ι), p i → Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) :
Continuous fun (x : X) => ∏ᶠ (i : ι) (_ : p i), f i x
source
theorem continuous_finsum_cond {ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} {p : ι → Prop} (hc : ∀ (i : ι), p i → Continuous (f i)) (hf : LocallyFinite fun (i : ι) => Function.support (f i)) :
Continuous fun (x : X) => ∑ᶠ (i : ι) (_ : p i), f i x
source
instance instContinuousAddAdditiveOfContinuousMul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] :
ContinuousAdd (Additive M)
source
instance instContinuousMulMultiplicativeOfContinuousAdd {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] :
ContinuousMul (Multiplicative M)
source
theorem continuousMul_sInf {M : Type u_3} [Mul M] {ts : Set (TopologicalSpace M)} (h : ∀ t ∈ ts, ContinuousMul M) :
ContinuousMul M
source
theorem continuousAdd_sInf {M : Type u_3} [Add M] {ts : Set (TopologicalSpace M)} (h : ∀ t ∈ ts, ContinuousAdd M) :
ContinuousAdd M
source
theorem continuousMul_iInf {M : Type u_3} {ι' : Sort u_6} [Mul M] {ts : ι' → TopologicalSpace M} (h' : ∀ (i : ι'), ContinuousMul M) :
ContinuousMul M
source
theorem continuousAdd_iInf {M : Type u_3} {ι' : Sort u_6} [Add M] {ts : ι' → TopologicalSpace M} (h' : ∀ (i : ι'), ContinuousAdd M) :
ContinuousAdd M
source
theorem continuousMul_inf {M : Type u_3} [Mul M] {t₁ t₂ : TopologicalSpace M} (h₁ : ContinuousMul M) (h₂ : ContinuousMul M) :
ContinuousMul M
source
theorem continuousAdd_inf {M : Type u_3} [Add M] {t₁ t₂ : TopologicalSpace M} (h₁ : ContinuousAdd M) (h₂ : ContinuousAdd M) :
ContinuousAdd M
source
def ContinuousMap.mulRight {X : Type u_5} [TopologicalSpace X] [Mul X] [ContinuousMul X] (x : X) :
C(X, X)

The continuous map `fun y => y * x`

Equations

- ContinuousMap.mulRight x = { toFun := fun (b : X) => b * x, continuous_toFun := ⋯ }

Instances For

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

The continuous map `fun y => y + x`

Equations

- ContinuousMap.addRight x = { toFun := fun (b : X) => b + x, continuous_toFun := ⋯ }

Instances For

source
@[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
source
@[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
source
def ContinuousMap.mulLeft {X : Type u_5} [TopologicalSpace X] [Mul X] [ContinuousMul X] (x : X) :
C(X, X)

The continuous map `fun y => x * y`

Equations

- ContinuousMap.mulLeft x = { toFun := fun (b : X) => x * b, continuous_toFun := ⋯ }

Instances For

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

The continuous map `fun y => x + y`

Equations

- ContinuousMap.addLeft x = { toFun := fun (b : X) => x + b, continuous_toFun := ⋯ }

Instances For

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