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_zero {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [Zero M] :

Continuous 0

source

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

Continuous 1

source

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

Prop

Basic hypothesis to talk about a topological additive monoid or a topological additive semigroup. A topological additive monoid over M, for example, is obtained by requiring both the instances AddMonoid M and ContinuousAdd M.

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

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

Instances

source

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

Prop

Basic hypothesis to talk about a topological monoid or a topological semigroup. A topological monoid over M, for example, is obtained by requiring both the instances Monoid M and ContinuousMul M.

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

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

Instances

source

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

ContinuousAdd Mᵒᵈ

Equations

⋯ = inst

source

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

ContinuousMul Mᵒᵈ

Equations

⋯ = inst

source

theorem continuous_add {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] :

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

source

theorem continuous_mul {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] :

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

source

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

ContinuousVAdd M M

Equations

⋯ = ⋯

source

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

ContinuousSMul M M

Equations

⋯ = ⋯

source

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

ContinuousVAdd Mᵃᵒᵖ M

Equations

⋯ = ⋯

source

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

ContinuousSMul Mᵐᵒᵖ M

Equations

⋯ = ⋯

source

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

Continuous fun (x : X) => f x + g x

source

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

Continuous fun (x : X) => f x * g x

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_left {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a : M) :

Continuous fun (b : M) => a * b

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 continuous_mul_right {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a : M) :

Continuous fun (b : M) => b * a

source

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

ContinuousOn (fun (x : X) => f x + g x) s

source

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

ContinuousOn (fun (x : X) => f x * g x) s

source

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

source

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

source

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

source

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

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 : Filter.Tendsto (fun (k : α) => f k) l (nhds c)) :

Filter.Tendsto (fun (k : α) => b + f k) l (nhds (b + c))

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 : Filter.Tendsto (fun (k : α) => f k) l (nhds c)) :

Filter.Tendsto (fun (k : α) => b * f k) l (nhds (b * c))

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 : Filter.Tendsto (fun (k : α) => f k) l (nhds c)) :

Filter.Tendsto (fun (k : α) => f k + b) l (nhds (c + b))

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 : Filter.Tendsto (fun (k : α) => f k) l (nhds c)) :

Filter.Tendsto (fun (k : α) => f k * b) l (nhds (c * b))

source

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)

source

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)

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_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_add_nhds_zero {M : Type u_6} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] (a : M) :

nhds a + nhds 0 = 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

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

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 𝕜] [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)))

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 𝕜] [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)))

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 𝕜] [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)))

source

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

source

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

AddUnits N

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

Equations

Filter.Tendsto.addUnits h₁ h₂ = { val := r₁, neg := r₂, val_neg := ⋯, neg_val := ⋯ }

Instances For

source

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

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

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

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

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

source

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

Nˣ

Construct a unit from limits of units and their inverses.

Equations

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

Instances For

source

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

ContinuousAt (fun (x : X) => f x + g x) x

source

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

ContinuousAt (fun (x : X) => f x * g x) x

source

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

ContinuousWithinAt (fun (x : X) => f x + g x) s x

source

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

ContinuousWithinAt (fun (x : X) => f x * g x) s x

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)

Equations

⋯ = ⋯

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)

Equations

⋯ = ⋯

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)

Equations

⋯ = ⋯

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)

Equations

⋯ = ⋯

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.

Equations

⋯ = ⋯

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.

Equations

⋯ = ⋯

source

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

ContinuousAdd N

Equations

⋯ = ⋯

source

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

ContinuousMul N

Equations

⋯ = ⋯

source

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

ContinuousAdd M

source

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

ContinuousMul M

source

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

ContinuousAdd M

source

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

ContinuousMul M

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_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_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

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

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 = { toZeroHom := { toFun := f, map_zero' := ⋯ }, map_add' := ⋯ }

Instances For

source

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}

source

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}

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 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 = { toOneHom := { toFun := f, map_one' := ⋯ }, map_mul' := ⋯ }

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) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :

M₁ →+ M₂

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

Equations

addMonoidHomOfTendsto f g h = addMonoidHomOfMemClosureRangeCoe f ⋯

Instances For

source

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)

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) [Filter.NeBot l] (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) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :

⇑(addMonoidHomOfTendsto f g h) = 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) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :

M₁ →* M₂

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

Equations

monoidHomOfTendsto f g h = monoidHomOfMemClosureRangeCoe f ⋯

Instances For

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 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 Inducing.continuousAdd {M : Type u_6} {N : Type u_7} {F : Type u_8} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousAdd N] (f : F) (hf : Inducing ⇑f) :

ContinuousAdd M

source

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

ContinuousMul M

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

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

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

ContinuousAdd ↥S

Equations

⋯ = ⋯

source

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

ContinuousMul ↥S

Equations

⋯ = ⋯

source

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

ContinuousAdd ↥S

Equations

⋯ = ⋯

source

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

ContinuousMul ↥S

Equations

⋯ = ⋯

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_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

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 ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s) → Prop) :

∀ (x : ∃ (V : Set M), IsOpen V ∧ 0 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s), (∀ (V : Set M) (Vo : IsOpen V) (V1 : 0 ∈ V) (hV : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ s), motive ⋯) → motive x

Equations

⋯ = ⋯

Instances For

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_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_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 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 AddSubmonoid.top_closure_add_self_subset {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :

closure ↑s + closure ↑s ⊆ closure ↑s

source

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

closure ↑s * closure ↑s ⊆ closure ↑s

source

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

closure ↑s + closure ↑s = closure ↑s

source

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

closure ↑s * closure ↑s = closure ↑s

source

theorem AddSubmonoid.topologicalClosure.proof_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (s : AddSubmonoid M) :

∀ {a b : M}, a ∈ closure ↑s → b ∈ closure ↑s → a + b ∈ closure ↑s

source

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

0 ∈ closure ↑s

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

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

Instances For

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

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

Instances For

source

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

↑(AddSubmonoid.topologicalClosure s) = closure ↑s

source

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

↑(Submonoid.topologicalClosure s) = closure ↑s

source

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

s ≤ AddSubmonoid.topologicalClosure s

source

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

s ≤ Submonoid.topologicalClosure s

source

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

IsClosed ↑(AddSubmonoid.topologicalClosure s)

source

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

IsClosed ↑(Submonoid.topologicalClosure s)

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

AddSubmonoid.topologicalClosure s ≤ t

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

Submonoid.topologicalClosure s ≤ t

source

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

source

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

source

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

AddCommMonoid ↥(AddSubmonoid.topologicalClosure s)

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

Equations

AddSubmonoid.addCommMonoidTopologicalClosure s hs = let __src := AddSubmonoid.toAddMonoid (AddSubmonoid.topologicalClosure s); AddCommMonoid.mk ⋯

Instances For

source

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

CommMonoid ↥(Submonoid.topologicalClosure s)

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

Equations

Submonoid.commMonoidTopologicalClosure s hs = let __src := Submonoid.toMonoid (Submonoid.topologicalClosure s); CommMonoid.mk ⋯

Instances For

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

source

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)

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.sum (List.map (fun (c : ι) => f c b) l)) x (nhds (List.sum (List.map a l)))

source

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

∀ (x_1 : List ι) (x_2 : ∀ i ∈ x_1, Filter.Tendsto (f i) x (nhds (a i))), (∀ (x : ∀ i ∈ [], Filter.Tendsto (f i) x (nhds (a i))), motive [] x) → (∀ (f_1 : ι) (l : List ι) (h : ∀ i ∈ f_1 :: l, Filter.Tendsto (f i) x (nhds (a i))), motive (f_1 :: l) h) → motive x_1 x_2

Equations

⋯ = ⋯

Instances For

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.prod (List.map (fun (c : ι) => f c b) l)) x (nhds (List.prod (List.map a l)))

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.sum (List.map (fun (i : ι) => f i a) l)

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.prod (List.map (fun (i : ι) => f i a) l)

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.sum (List.map (fun (i : ι) => f i a) l)) t

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.prod (List.map (fun (i : ι) => f i a) l)) t

source

theorem continuous_nsmul {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (n : ℕ) :

Continuous fun (a : M) => n • a

source

abbrev continuous_nsmul.match_1 (motive : ℕ → Prop) :

∀ (x : ℕ), (Unit → motive 0) → (∀ (k : ℕ), motive (Nat.succ k)) → motive x

Equations

⋯ = ⋯

Instances For

source

theorem continuous_pow {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (n : ℕ) :

Continuous fun (a : M) => a ^ n

source

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

ContinuousConstSMul ℕ A

Equations

⋯ = ⋯

source

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

ContinuousSMul ℕ A

Equations

⋯ = ⋯

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 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 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 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 continuousAt_nsmul {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (x : M) (n : ℕ) :

ContinuousAt (fun (x : M) => n • x) x

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

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 : Filter.Tendsto f l (nhds x)) (n : ℕ) :

Filter.Tendsto (fun (x : α) => f x ^ n) l (nhds (x ^ n))

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

source

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.

source

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

ContinuousConstVAdd R A

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

Equations

⋯ = ⋯

source

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

ContinuousConstSMul R A

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

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

Equations

⋯ = ⋯

source

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

ContinuousConstVAdd R A

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

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

Equations

⋯ = ⋯

source

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

ContinuousConstSMul R A

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

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

Equations

⋯ = ⋯

source

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

ContinuousAdd αᵃᵒᵖ

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

Equations

⋯ = ⋯

source

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

ContinuousMul αᵐᵒᵖ

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

Equations

⋯ = ⋯

source

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

ContinuousAdd (AddUnits α)

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

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

Equations

⋯ = ⋯

source

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

ContinuousMul αˣ

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

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

Equations

⋯ = ⋯

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 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 AddSubmonoid.mem_nhds_zero {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] (S : AddSubmonoid M) (oS : IsOpen ↑S) :

↑S ∈ nhds 0

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 tendsto_multiset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) :

(∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun (b : α) => Multiset.sum (Multiset.map (fun (c : ι) => f c b) s)) x (nhds (Multiset.sum (Multiset.map a s)))

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.prod (Multiset.map (fun (c : ι) => f c b) s)) x (nhds (Multiset.prod (Multiset.map a s)))

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 : α) => Finset.sum s fun (c : ι) => f c b) x (nhds (Finset.sum s fun (c : ι) => a c))

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 : α) => Finset.prod s fun (c : ι) => f c b) x (nhds (Finset.prod s fun (c : ι) => a c))

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.sum (Multiset.map (fun (i : ι) => f i a) s)

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.prod (Multiset.map (fun (i : ι) => f i a) s)

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.sum (Multiset.map (fun (i : ι) => f i a) s)) t

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.prod (Multiset.map (fun (i : ι) => f i a) s)) t

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) => Finset.sum s fun (i : ι) => f i a

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) => Finset.prod s fun (i : ι) => f i a

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) => Finset.sum s fun (i : ι) => f i a) t

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) => Finset.prod s fun (i : ι) => f i a) t

source

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

(Finset.sum s fun (i : ι) => f i) =ᶠ[l] Finset.sum s fun (i : ι) => g i

source

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

(Finset.prod s fun (i : ι) => f i) =ᶠ[l] Finset.prod s fun (i : ι) => g i

source

theorem LocallyFinite.exists_finset_support {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [AddCommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.support (f i)) (x₀ : X) :

∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x₀, (Function.support fun (i : ι) => f i x) ⊆ ↑I

source

theorem LocallyFinite.exists_finset_mulSupport {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [CommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun (i : ι) => Function.mulSupport (f i)) (x₀ : X) :

∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x₀, (Function.mulSupport fun (i : ι) => f i x) ⊆ ↑I

source

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

∀ (x_1 : ∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) ⊆ ↑I), (∀ (I : Finset ι) (hI : ∀ᶠ (x : X) in nhds x, (Function.support fun (i : ι) => f i x) ⊆ ↑I), motive ⋯) → motive x_1

Equations

⋯ = ⋯

Instances For

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, (finsum fun (i : ι) => f i y) = Finset.sum s fun (i : ι) => f i y

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, (finprod fun (i : ι) => f i y) = Finset.prod s fun (i : ι) => f i y

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) => finsum fun (i : ι) => f i x

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) => finprod fun (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) => finsum fun (i : ι) => finsum fun (x_1 : p 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) => finprod fun (i : ι) => finprod fun (x_1 : p i) => f i x

source

instance instContinuousAddAdditiveInstTopologicalSpaceAdditiveAdd {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] :

ContinuousAdd (Additive M)

Equations

⋯ = ⋯

source

instance instContinuousMulMultiplicativeInstTopologicalSpaceMultiplicativeMul {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] :

ContinuousMul (Multiplicative M)

Equations

⋯ = ⋯

source

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

ContinuousAdd 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_iInf {M : Type u_3} {ι' : Sort u_6} [Add M] {ts : ι' → TopologicalSpace M} (h' : ∀ (i : ι'), 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_inf {M : Type u_3} [Add M] {t₁ : TopologicalSpace M} {t₂ : TopologicalSpace M} (h₁ : ContinuousAdd M) (h₂ : ContinuousAdd M) :

ContinuousAdd M

source

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

ContinuousMul M

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

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

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

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

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

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

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

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

Documentation

Mathlib.Topology.Algebra.Monoid

Theory of topological monoids #