Theory of topological monoids #
In this file we define mixin classes ContinuousMul and ContinuousAdd. While in many
applications the underlying type is a monoid (multiplicative or additive), we do not require this in
the definitions.
theorem
continuous_zero
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[Zero M]
:
theorem
continuous_one
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[One M]
:
Basic hypothesis to talk about a topological additive monoid or a topological additive
semigroup. A topological additive monoid over M, for example, is obtained by requiring both the
instances AddMonoid M and ContinuousAdd M.
Continuity in only the left/right argument can be stated using
ContinuousConstVAdd α α/ContinuousConstVAdd αᵐᵒᵖ α.
- continuous_add : Continuous fun (p : M × M) => p.1 + p.2
Instances
theorem
ContinuousAdd.continuous_add
{M : Type u}
[TopologicalSpace M]
[Add M]
[self : ContinuousAdd M]
:
Continuous fun (p : M × M) => p.1 + p.2
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
theorem
ContinuousMul.continuous_mul
{M : Type u}
[TopologicalSpace M]
[Mul M]
[self : ContinuousMul M]
:
Continuous fun (p : M × M) => p.1 * p.2
Equations
- ⋯ = inst
Equations
- ⋯ = inst
theorem
continuous_add
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
Continuous fun (p : M × M) => p.1 + p.2
theorem
continuous_mul
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
Continuous fun (p : M × M) => p.1 * p.2
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
instance
ContinuousAdd.to_continuousVAdd
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
ContinuousVAdd M M
Equations
- ⋯ = ⋯
instance
ContinuousMul.to_continuousSMul
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
ContinuousSMul M M
Equations
- ⋯ = ⋯
instance
ContinuousAdd.to_continuousVAdd_op
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
Equations
- ⋯ = ⋯
instance
ContinuousMul.to_continuousSMul_op
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
Equations
- ⋯ = ⋯
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
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
theorem
continuous_add_left
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
(a : M)
:
Continuous fun (b : M) => a + b
theorem
continuous_mul_left
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
(a : M)
:
Continuous fun (b : M) => a * b
theorem
continuous_add_right
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
(a : M)
:
Continuous fun (b : M) => b + a
theorem
continuous_mul_right
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
(a : M)
:
Continuous fun (b : M) => b * a
theorem
ContinuousOn.add
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{f : 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
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
theorem
Filter.Tendsto.add
{α : Type u_2}
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{f : α → M}
{g : α → M}
{x : Filter α}
{a : M}
{b : M}
(hf : Filter.Tendsto f x (nhds a))
(hg : Filter.Tendsto g x (nhds b))
:
Filter.Tendsto (fun (x : α) => f x + g x) x (nhds (a + b))
theorem
Filter.Tendsto.mul
{α : Type u_2}
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{f : α → M}
{g : α → M}
{x : Filter α}
{a : M}
{b : M}
(hf : Filter.Tendsto f x (nhds a))
(hg : Filter.Tendsto g x (nhds b))
:
Filter.Tendsto (fun (x : α) => f x * g x) x (nhds (a * b))
theorem
Filter.Tendsto.const_add
{α : Type u_2}
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
(b : M)
{c : M}
{f : α → M}
{l : Filter α}
(h : Filter.Tendsto (fun (k : α) => f k) l (nhds c))
:
Filter.Tendsto (fun (k : α) => b + f k) l (nhds (b + c))
theorem
Filter.Tendsto.const_mul
{α : Type u_2}
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
(b : M)
{c : M}
{f : α → M}
{l : Filter α}
(h : Filter.Tendsto (fun (k : α) => f k) l (nhds c))
:
Filter.Tendsto (fun (k : α) => b * f k) l (nhds (b * c))
theorem
Filter.Tendsto.add_const
{α : Type u_2}
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
(b : M)
{c : M}
{f : α → M}
{l : Filter α}
(h : Filter.Tendsto (fun (k : α) => f k) l (nhds c))
:
Filter.Tendsto (fun (k : α) => f k + b) l (nhds (c + b))
theorem
Filter.Tendsto.mul_const
{α : Type u_2}
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
(b : M)
{c : M}
{f : α → M}
{l : Filter α}
(h : Filter.Tendsto (fun (k : α) => f k) l (nhds c))
:
Filter.Tendsto (fun (k : α) => f k * b) l (nhds (c * b))
@[simp]
theorem
nhds_zero_add_nhds
{M : Type u_6}
[AddZeroClass M]
[TopologicalSpace M]
[ContinuousAdd M]
(a : M)
:
@[simp]
theorem
nhds_one_mul_nhds
{M : Type u_6}
[MulOneClass M]
[TopologicalSpace M]
[ContinuousMul M]
(a : M)
:
@[simp]
theorem
nhds_add_nhds_zero
{M : Type u_6}
[AddZeroClass M]
[TopologicalSpace M]
[ContinuousAdd M]
(a : M)
:
@[simp]
theorem
nhds_mul_nhds_one
{M : Type u_6}
[MulOneClass M]
[TopologicalSpace M]
[ContinuousMul M]
(a : M)
:
theorem
Filter.TendstoNhdsWithinIoi.const_mul
{α : Type u_2}
{𝕜 : Type u_6}
[Preorder 𝕜]
[Zero 𝕜]
[Mul 𝕜]
[TopologicalSpace 𝕜]
[ContinuousMul 𝕜]
{l : Filter α}
{f : α → 𝕜}
{b : 𝕜}
{c : 𝕜}
(hb : 0 < b)
[PosMulStrictMono 𝕜]
[PosMulReflectLT 𝕜]
(h : Filter.Tendsto f l (nhdsWithin c (Set.Ioi c)))
:
Filter.Tendsto (fun (a : α) => b * f a) l (nhdsWithin (b * c) (Set.Ioi (b * c)))
theorem
Filter.TendstoNhdsWithinIio.const_mul
{α : Type u_2}
{𝕜 : Type u_6}
[Preorder 𝕜]
[Zero 𝕜]
[Mul 𝕜]
[TopologicalSpace 𝕜]
[ContinuousMul 𝕜]
{l : Filter α}
{f : α → 𝕜}
{b : 𝕜}
{c : 𝕜}
(hb : 0 < b)
[PosMulStrictMono 𝕜]
[PosMulReflectLT 𝕜]
(h : Filter.Tendsto f l (nhdsWithin c (Set.Iio c)))
:
Filter.Tendsto (fun (a : α) => b * f a) l (nhdsWithin (b * c) (Set.Iio (b * c)))
theorem
Filter.TendstoNhdsWithinIoi.mul_const
{α : Type u_2}
{𝕜 : Type u_6}
[Preorder 𝕜]
[Zero 𝕜]
[Mul 𝕜]
[TopologicalSpace 𝕜]
[ContinuousMul 𝕜]
{l : Filter α}
{f : α → 𝕜}
{b : 𝕜}
{c : 𝕜}
(hb : 0 < b)
[MulPosStrictMono 𝕜]
[MulPosReflectLT 𝕜]
(h : Filter.Tendsto f l (nhdsWithin c (Set.Ioi c)))
:
Filter.Tendsto (fun (a : α) => f a * b) l (nhdsWithin (c * b) (Set.Ioi (c * b)))
theorem
Filter.TendstoNhdsWithinIio.mul_const
{α : Type u_2}
{𝕜 : Type u_6}
[Preorder 𝕜]
[Zero 𝕜]
[Mul 𝕜]
[TopologicalSpace 𝕜]
[ContinuousMul 𝕜]
{l : Filter α}
{f : α → 𝕜}
{b : 𝕜}
{c : 𝕜}
(hb : 0 < b)
[MulPosStrictMono 𝕜]
[MulPosReflectLT 𝕜]
(h : Filter.Tendsto f l (nhdsWithin c (Set.Iio c)))
:
Filter.Tendsto (fun (a : α) => f a * b) l (nhdsWithin (c * b) (Set.Iio (c * b)))
theorem
Specializes.add
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{a : M}
{b : M}
{c : M}
{d : M}
(hab : a ⤳ b)
(hcd : c ⤳ d)
:
theorem
Specializes.mul
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{a : M}
{b : M}
{c : M}
{d : M}
(hab : a ⤳ b)
(hcd : c ⤳ d)
:
theorem
Inseparable.add
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{a : M}
{b : M}
{c : M}
{d : M}
(hab : Inseparable a b)
(hcd : Inseparable c d)
:
Inseparable (a + c) (b + d)
theorem
Inseparable.mul
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{a : M}
{b : M}
{c : M}
{d : M}
(hab : Inseparable a b)
(hcd : Inseparable c d)
:
Inseparable (a * c) (b * d)
theorem
Specializes.nsmul
{M : Type u_6}
[AddMonoid M]
[TopologicalSpace M]
[ContinuousAdd M]
{a : M}
{b : M}
(h : a ⤳ b)
(n : ℕ)
:
theorem
Specializes.pow
{M : Type u_6}
[Monoid M]
[TopologicalSpace M]
[ContinuousMul M]
{a : M}
{b : M}
(h : a ⤳ b)
(n : ℕ)
:
theorem
Inseparable.nsmul
{M : Type u_6}
[AddMonoid M]
[TopologicalSpace M]
[ContinuousAdd M]
{a : M}
{b : M}
(h : Inseparable a b)
(n : ℕ)
:
Inseparable (n • a) (n • b)
theorem
Inseparable.pow
{M : Type u_6}
[Monoid M]
[TopologicalSpace M]
[ContinuousMul M]
{a : M}
{b : M}
(h : Inseparable a b)
(n : ℕ)
:
Inseparable (a ^ n) (b ^ n)
theorem
Filter.Tendsto.addUnits.proof_1
{ι : Type u_2}
{N : Type u_1}
[TopologicalSpace N]
[AddMonoid N]
[ContinuousAdd N]
[T2Space N]
{f : ι → AddUnits N}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[l.NeBot]
(h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂))
:
theorem
Filter.Tendsto.addUnits.proof_2
{ι : Type u_2}
{N : Type u_1}
[TopologicalSpace N]
[AddMonoid N]
[ContinuousAdd N]
[T2Space N]
{f : ι → AddUnits N}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[l.NeBot]
(h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂))
:
def
Filter.Tendsto.addUnits
{ι : Type u_1}
{N : Type u_4}
[TopologicalSpace N]
[AddMonoid N]
[ContinuousAdd N]
[T2Space N]
{f : ι → AddUnits N}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[l.NeBot]
(h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂))
:
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
@[simp]
theorem
Filter.Tendsto.val_neg_addUnits
{ι : Type u_1}
{N : Type u_4}
[TopologicalSpace N]
[AddMonoid N]
[ContinuousAdd N]
[T2Space N]
{f : ι → AddUnits N}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[l.NeBot]
(h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂))
:
@[simp]
theorem
Filter.Tendsto.val_units
{ι : Type u_1}
{N : Type u_4}
[TopologicalSpace N]
[Monoid N]
[ContinuousMul N]
[T2Space N]
{f : ι → Nˣ}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[l.NeBot]
(h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂))
:
↑(h₁.units h₂) = r₁
@[simp]
theorem
Filter.Tendsto.val_inv_units
{ι : Type u_1}
{N : Type u_4}
[TopologicalSpace N]
[Monoid N]
[ContinuousMul N]
[T2Space N]
{f : ι → Nˣ}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[l.NeBot]
(h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂))
:
@[simp]
theorem
Filter.Tendsto.val_addUnits
{ι : Type u_1}
{N : Type u_4}
[TopologicalSpace N]
[AddMonoid N]
[ContinuousAdd N]
[T2Space N]
{f : ι → AddUnits N}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[l.NeBot]
(h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun (x : ι) => ↑(-f x)) l (nhds r₂))
:
↑(h₁.addUnits h₂) = r₁
def
Filter.Tendsto.units
{ι : Type u_1}
{N : Type u_4}
[TopologicalSpace N]
[Monoid N]
[ContinuousMul N]
[T2Space N]
{f : ι → Nˣ}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[l.NeBot]
(h₁ : Filter.Tendsto (fun (x : ι) => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun (x : ι) => ↑(f x)⁻¹) l (nhds r₂))
:
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
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
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
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
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
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
- ⋯ = ⋯
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
- ⋯ = ⋯
instance
Pi.continuousAdd
{ι : Type u_1}
{C : ι → Type u_6}
[(i : ι) → TopologicalSpace (C i)]
[(i : ι) → Add (C i)]
[∀ (i : ι), ContinuousAdd (C i)]
:
ContinuousAdd ((i : ι) → C i)
Equations
- ⋯ = ⋯
instance
Pi.continuousMul
{ι : Type u_1}
{C : ι → Type u_6}
[(i : ι) → TopologicalSpace (C i)]
[(i : ι) → Mul (C i)]
[∀ (i : ι), ContinuousMul (C i)]
:
ContinuousMul ((i : ι) → C i)
Equations
- ⋯ = ⋯
instance
Pi.continuousAdd'
{ι : Type u_1}
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
ContinuousAdd (ι → M)
A version of Pi.continuousAdd for non-dependent functions. It is needed
because sometimes Lean fails to use Pi.continuousAdd for non-dependent functions.
Equations
- ⋯ = ⋯
instance
Pi.continuousMul'
{ι : Type u_1}
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
ContinuousMul (ι → M)
A version of Pi.continuousMul for non-dependent functions. It is needed because sometimes
Lean 3 fails to use Pi.continuousMul for non-dependent functions.
Equations
- ⋯ = ⋯
@[instance 100]
instance
continuousAdd_of_discreteTopology
{N : Type u_4}
[TopologicalSpace N]
[Add N]
[DiscreteTopology N]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
continuousMul_of_discreteTopology
{N : Type u_4}
[TopologicalSpace N]
[Mul N]
[DiscreteTopology N]
:
Equations
- ⋯ = ⋯
theorem
ContinuousAdd.of_nhds_zero
{M : Type u}
[AddMonoid M]
[TopologicalSpace M]
(hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : M) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0))
(hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x₀ + x) (nhds 0))
(hright : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x + x₀) (nhds 0))
:
theorem
ContinuousMul.of_nhds_one
{M : Type u}
[Monoid M]
[TopologicalSpace M]
(hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : M) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1))
(hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x₀ * x) (nhds 1))
(hright : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x * x₀) (nhds 1))
:
theorem
continuousAdd_of_comm_of_nhds_zero
(M : Type u)
[AddCommMonoid M]
[TopologicalSpace M]
(hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : M) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0))
(hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x₀ + x) (nhds 0))
:
theorem
continuousMul_of_comm_of_nhds_one
(M : Type u)
[CommMonoid M]
[TopologicalSpace M]
(hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : M) => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1))
(hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun (x : M) => x₀ * x) (nhds 1))
:
theorem
isClosed_setOf_map_zero
(M₁ : Type u_6)
(M₂ : Type u_7)
[TopologicalSpace M₂]
[T2Space M₂]
[Zero M₁]
[Zero M₂]
:
theorem
isClosed_setOf_map_one
(M₁ : Type u_6)
(M₂ : Type u_7)
[TopologicalSpace M₂]
[T2Space M₂]
[One M₁]
[One M₂]
:
theorem
isClosed_setOf_map_add
(M₁ : Type u_6)
(M₂ : Type u_7)
[TopologicalSpace M₂]
[T2Space M₂]
[Add M₁]
[Add M₂]
[ContinuousAdd M₂]
:
theorem
isClosed_setOf_map_mul
(M₁ : Type u_6)
(M₂ : Type u_7)
[TopologicalSpace M₂]
[T2Space M₂]
[Mul M₁]
[Mul M₂]
[ContinuousMul M₂]
:
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
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))
:
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))
:
@[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
@[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
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
theorem
addMonoidHomOfTendsto.proof_1
{α : Type u_4}
{M₁ : Type u_1}
{M₂ : Type u_2}
[TopologicalSpace M₂]
{F : Type u_3}
[FunLike F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[l.NeBot]
(h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f))
:
def
addMonoidHomOfTendsto
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace M₂]
[T2Space M₂]
[AddZeroClass M₁]
[AddZeroClass M₂]
[ContinuousAdd M₂]
{F : Type u_8}
[FunLike F M₁ M₂]
[AddMonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[l.NeBot]
(h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f))
:
M₁ →+ M₂
Construct a bundled additive monoid homomorphism from a pointwise limit of additive monoid homomorphisms
Equations
Instances For
@[simp]
theorem
addMonoidHomOfTendsto_apply
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace M₂]
[T2Space M₂]
[AddZeroClass M₁]
[AddZeroClass M₂]
[ContinuousAdd M₂]
{F : Type u_8}
[FunLike F M₁ M₂]
[AddMonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[l.NeBot]
(h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f))
:
⇑(addMonoidHomOfTendsto f g h) = f
@[simp]
theorem
monoidHomOfTendsto_apply
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace M₂]
[T2Space M₂]
[MulOneClass M₁]
[MulOneClass M₂]
[ContinuousMul M₂]
{F : Type u_8}
[FunLike F M₁ M₂]
[MonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[l.NeBot]
(h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f))
:
⇑(monoidHomOfTendsto f g h) = f
def
monoidHomOfTendsto
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace M₂]
[T2Space M₂]
[MulOneClass M₁]
[MulOneClass M₂]
[ContinuousMul M₂]
{F : Type u_8}
[FunLike F M₁ M₂]
[MonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[l.NeBot]
(h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f))
:
M₁ →* M₂
Construct a bundled monoid homomorphism from a pointwise limit of monoid homomorphisms.
Equations
- monoidHomOfTendsto f g h = monoidHomOfMemClosureRangeCoe f ⋯
Instances For
theorem
AddMonoidHom.isClosed_range_coe
(M₁ : Type u_6)
(M₂ : Type u_7)
[TopologicalSpace M₂]
[T2Space M₂]
[AddZeroClass M₁]
[AddZeroClass M₂]
[ContinuousAdd M₂]
:
theorem
MonoidHom.isClosed_range_coe
(M₁ : Type u_6)
(M₂ : Type u_7)
[TopologicalSpace M₂]
[T2Space M₂]
[MulOneClass M₁]
[MulOneClass M₂]
[ContinuousMul M₂]
:
theorem
Inducing.continuousAdd
{M : Type u_6}
{N : Type u_7}
{F : Type u_8}
[Add M]
[Add N]
[FunLike F M N]
[AddHomClass F M N]
[TopologicalSpace M]
[TopologicalSpace N]
[ContinuousAdd N]
(f : F)
(hf : Inducing ⇑f)
:
theorem
Inducing.continuousMul
{M : Type u_6}
{N : Type u_7}
{F : Type u_8}
[Mul M]
[Mul N]
[FunLike F M N]
[MulHomClass F M N]
[TopologicalSpace M]
[TopologicalSpace N]
[ContinuousMul N]
(f : F)
(hf : Inducing ⇑f)
:
theorem
continuousAdd_induced
{M : Type u_6}
{N : Type u_7}
{F : Type u_8}
[Add M]
[Add N]
[FunLike F M N]
[AddHomClass F M N]
[TopologicalSpace N]
[ContinuousAdd N]
(f : F)
:
theorem
continuousMul_induced
{M : Type u_6}
{N : Type u_7}
{F : Type u_8}
[Mul M]
[Mul N]
[FunLike F M N]
[MulHomClass F M N]
[TopologicalSpace N]
[ContinuousMul N]
(f : F)
:
instance
AddSubsemigroup.continuousAdd
{M : Type u_3}
[TopologicalSpace M]
[AddSemigroup M]
[ContinuousAdd M]
(S : AddSubsemigroup M)
:
Equations
- ⋯ = ⋯
instance
Subsemigroup.continuousMul
{M : Type u_3}
[TopologicalSpace M]
[Semigroup M]
[ContinuousMul M]
(S : Subsemigroup M)
:
Equations
- ⋯ = ⋯
instance
AddSubmonoid.continuousAdd
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(S : AddSubmonoid M)
:
Equations
- ⋯ = ⋯
instance
Submonoid.continuousMul
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(S : Submonoid M)
:
Equations
- ⋯ = ⋯
theorem
exists_open_nhds_zero_half
{M : Type u_3}
[TopologicalSpace M]
[AddZeroClass M]
[ContinuousAdd M]
{s : Set M}
(hs : s ∈ nhds 0)
:
theorem
exists_open_nhds_one_split
{M : Type u_3}
[TopologicalSpace M]
[MulOneClass M]
[ContinuousMul M]
{s : Set M}
(hs : s ∈ nhds 1)
:
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)
:
Equations
- ⋯ = ⋯
Instances For
theorem
exists_nhds_zero_half
{M : Type u_3}
[TopologicalSpace M]
[AddZeroClass M]
[ContinuousAdd M]
{s : Set M}
(hs : s ∈ nhds 0)
:
theorem
exists_nhds_one_split
{M : Type u_3}
[TopologicalSpace M]
[MulOneClass M]
[ContinuousMul M]
{s : Set M}
(hs : s ∈ nhds 1)
:
theorem
exists_open_nhds_zero_add_subset
{M : Type u_3}
[TopologicalSpace M]
[AddZeroClass M]
[ContinuousAdd M]
{U : Set M}
(hU : U ∈ nhds 0)
:
Given an open neighborhood U of 0 there is an open neighborhood V of 0
such that V + V ⊆ U.
theorem
exists_open_nhds_one_mul_subset
{M : Type u_3}
[TopologicalSpace M]
[MulOneClass M]
[ContinuousMul M]
{U : Set M}
(hU : U ∈ nhds 1)
:
Given a neighborhood U of 1 there is an open neighborhood V of 1
such that V * V ⊆ U.
theorem
AddSubmonoid.top_closure_add_self_subset
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
theorem
Submonoid.top_closure_mul_self_subset
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
theorem
AddSubmonoid.top_closure_add_self_eq
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
theorem
Submonoid.top_closure_mul_self_eq
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
theorem
AddSubmonoid.topologicalClosure.proof_1
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
theorem
AddSubmonoid.topologicalClosure.proof_2
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
(s : AddSubmonoid M)
:
def
AddSubmonoid.topologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
The (topological-space) closure of an additive submonoid of a space M with
ContinuousAdd is itself an additive submonoid.
Instances For
def
Submonoid.topologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
The (topological-space) closure of a submonoid of a space M with ContinuousMul is
itself a submonoid.
Instances For
theorem
AddSubmonoid.coe_topologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
theorem
Submonoid.coe_topologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
theorem
AddSubmonoid.le_topologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
s ≤ s.topologicalClosure
theorem
Submonoid.le_topologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
s ≤ s.topologicalClosure
theorem
AddSubmonoid.isClosed_topologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
IsClosed ↑s.topologicalClosure
theorem
Submonoid.isClosed_topologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
IsClosed ↑s.topologicalClosure
theorem
AddSubmonoid.topologicalClosure_minimal
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
{t : AddSubmonoid M}
(h : s ≤ t)
(ht : IsClosed ↑t)
:
s.topologicalClosure ≤ t
theorem
Submonoid.topologicalClosure_minimal
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
{t : Submonoid M}
(h : s ≤ t)
(ht : IsClosed ↑t)
:
s.topologicalClosure ≤ t
abbrev
AddSubmonoid.addCommMonoidTopologicalClosure.match_1
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
(motive : ↥s.topologicalClosure → Prop)
:
∀ (x : ↥s.topologicalClosure), (∀ (y : M) (hy : y ∈ s.topologicalClosure), motive ⟨y, hy⟩) → motive x
Equations
- ⋯ = ⋯
Instances For
theorem
AddSubmonoid.addCommMonoidTopologicalClosure.proof_1
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
[T2Space M]
(s : AddSubmonoid M)
(hs : ∀ (x y : ↥s), x + y = y + x)
:
def
AddSubmonoid.addCommMonoidTopologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
[T2Space M]
(s : AddSubmonoid M)
(hs : ∀ (x y : ↥s), x + y = y + x)
:
AddCommMonoid ↥s.topologicalClosure
If a submonoid of an additive topological monoid is commutative, then so is its topological closure.
Equations
- s.addCommMonoidTopologicalClosure hs = let __src := s.topologicalClosure.toAddMonoid; AddCommMonoid.mk ⋯
Instances For
def
Submonoid.commMonoidTopologicalClosure
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
[T2Space M]
(s : Submonoid M)
(hs : ∀ (x y : ↥s), x * y = y * x)
:
CommMonoid ↥s.topologicalClosure
If a submonoid of a topological monoid is commutative, then so is its topological closure.
Equations
- s.commMonoidTopologicalClosure hs = let __src := s.topologicalClosure.toMonoid; CommMonoid.mk ⋯
Instances For
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)
:
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)
:
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)
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
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)
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
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
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
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
theorem
continuous_nsmul
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(n : ℕ)
:
Continuous fun (a : M) => n • a
theorem
continuous_pow
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(n : ℕ)
:
Continuous fun (a : M) => a ^ n
instance
AddMonoid.continuousConstSMul_nat
{A : Type u_6}
[AddMonoid A]
[TopologicalSpace A]
[ContinuousAdd A]
:
Equations
- ⋯ = ⋯
instance
AddMonoid.continuousSMul_nat
{A : Type u_6}
[AddMonoid A]
[TopologicalSpace A]
[ContinuousAdd A]
:
Equations
- ⋯ = ⋯
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
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
theorem
continuousOn_nsmul
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{s : Set M}
(n : ℕ)
:
ContinuousOn (fun (x : M) => n • x) s
theorem
continuousOn_pow
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{s : Set M}
(n : ℕ)
:
ContinuousOn (fun (x : M) => x ^ n) s
theorem
continuousAt_nsmul
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(x : M)
(n : ℕ)
:
ContinuousAt (fun (x : M) => n • x) x
theorem
continuousAt_pow
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(x : M)
(n : ℕ)
:
ContinuousAt (fun (x : M) => x ^ n) x
theorem
Filter.Tendsto.nsmul
{α : Type u_2}
{M : Type u_3}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{l : Filter α}
{f : α → M}
{x : M}
(hf : Filter.Tendsto f l (nhds x))
(n : ℕ)
:
Filter.Tendsto (fun (x : α) => n • f x) l (nhds (n • x))
theorem
Filter.Tendsto.pow
{α : Type u_2}
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{l : Filter α}
{f : α → M}
{x : M}
(hf : Filter.Tendsto f l (nhds x))
(n : ℕ)
:
Filter.Tendsto (fun (x : α) => f x ^ n) l (nhds (x ^ n))
theorem
ContinuousWithinAt.nsmul
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : X → M}
{x : X}
{s : Set X}
(hf : ContinuousWithinAt f s x)
(n : ℕ)
:
ContinuousWithinAt (fun (x : X) => n • f x) s x
theorem
ContinuousWithinAt.pow
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : X → M}
{x : X}
{s : Set X}
(hf : ContinuousWithinAt f s x)
(n : ℕ)
:
ContinuousWithinAt (fun (x : X) => f x ^ n) s x
theorem
ContinuousAt.nsmul
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : X → M}
{x : X}
(hf : ContinuousAt f x)
(n : ℕ)
:
ContinuousAt (fun (x : X) => n • f x) x
theorem
ContinuousAt.pow
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : X → M}
{x : X}
(hf : ContinuousAt f x)
(n : ℕ)
:
ContinuousAt (fun (x : X) => f x ^ n) x
theorem
ContinuousOn.nsmul
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : X → M}
{s : Set X}
(hf : ContinuousOn f s)
(n : ℕ)
:
ContinuousOn (fun (x : X) => n • f x) s
theorem
ContinuousOn.pow
{M : Type u_3}
{X : Type u_5}
[TopologicalSpace X]
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : X → M}
{s : Set X}
(hf : ContinuousOn f s)
(n : ℕ)
:
ContinuousOn (fun (x : X) => f x ^ n) s
theorem
Filter.tendsto_cocompact_mul_left
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{a : M}
{b : M}
(ha : b * a = 1)
:
Filter.Tendsto (fun (x : M) => a * x) (Filter.cocompact M) (Filter.cocompact M)
Left-multiplication by a left-invertible element of a topological monoid is proper, i.e., inverse images of compact sets are compact.
theorem
Filter.tendsto_cocompact_mul_right
{M : Type u_3}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{a : M}
{b : M}
(ha : a * b = 1)
:
Filter.Tendsto (fun (x : M) => x * a) (Filter.cocompact M) (Filter.cocompact M)
Right-multiplication by a right-invertible element of a topological monoid is proper, i.e., inverse images of compact sets are compact.
@[instance 100]
instance
VAddAssocClass.continuousConstVAdd
{R : Type u_6}
{A : Type u_7}
[AddMonoid A]
[VAdd R A]
[VAddAssocClass R A A]
[TopologicalSpace A]
[ContinuousAdd A]
:
If R acts on A via A, then continuous addition implies
continuous affine addition by constants.
Equations
- ⋯ = ⋯
@[instance 100]
instance
IsScalarTower.continuousConstSMul
{R : Type u_6}
{A : Type u_7}
[Monoid A]
[SMul R A]
[IsScalarTower R A A]
[TopologicalSpace A]
[ContinuousMul A]
:
If R acts on A via A, then continuous multiplication implies continuous scalar
multiplication by constants.
Notably, this instances applies when R = A, or when [Algebra R A] is available.
Equations
- ⋯ = ⋯
@[instance 100]
instance
VAddCommClass.continuousConstVAdd
{R : Type u_6}
{A : Type u_7}
[AddMonoid A]
[VAdd R A]
[VAddCommClass R A A]
[TopologicalSpace A]
[ContinuousAdd A]
:
If the action of R on A commutes with left-addition, then
continuous addition implies continuous affine addition by constants.
Notably, this instances applies when R = Aᵃᵒᵖ.
Equations
- ⋯ = ⋯
@[instance 100]
instance
SMulCommClass.continuousConstSMul
{R : Type u_6}
{A : Type u_7}
[Monoid A]
[SMul R A]
[SMulCommClass R A A]
[TopologicalSpace A]
[ContinuousMul 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
- ⋯ = ⋯
instance
AddOpposite.instContinuousAdd
{α : Type u_2}
[TopologicalSpace α]
[Add α]
[ContinuousAdd α]
:
If addition is continuous in α, then it also is in αᵃᵒᵖ.
Equations
- ⋯ = ⋯
instance
MulOpposite.instContinuousMul
{α : Type u_2}
[TopologicalSpace α]
[Mul α]
[ContinuousMul α]
:
If multiplication is continuous in α, then it also is in αᵐᵒᵖ.
Equations
- ⋯ = ⋯
instance
AddUnits.instContinuousAdd
{α : Type u_2}
[TopologicalSpace α]
[AddMonoid α]
[ContinuousAdd α]
:
If addition on an additive monoid is continuous, then addition on the additive units of the monoid, with respect to the induced topology, is continuous.
Negation is also continuous, but we register this in a later file, Topology.Algebra.Group, because
the predicate ContinuousNeg has not yet been defined.
Equations
- ⋯ = ⋯
If multiplication on a monoid is continuous, then multiplication on the units of the monoid, with respect to the induced topology, is continuous.
Inversion is also continuous, but we register this in a later file, Topology.Algebra.Group,
because the predicate ContinuousInv has not yet been defined.
Equations
- ⋯ = ⋯
theorem
Continuous.addUnits_map
{M : Type u_3}
{N : Type u_4}
[AddMonoid M]
[AddMonoid N]
[TopologicalSpace M]
[TopologicalSpace N]
(f : M →+ N)
(hf : Continuous ⇑f)
:
Continuous ⇑(AddUnits.map f)
theorem
Continuous.units_map
{M : Type u_3}
{N : Type u_4}
[Monoid M]
[Monoid N]
[TopologicalSpace M]
[TopologicalSpace N]
(f : M →* N)
(hf : Continuous ⇑f)
:
Continuous ⇑(Units.map f)
theorem
AddSubmonoid.mem_nhds_zero
{M : Type u_3}
[TopologicalSpace M]
[AddCommMonoid M]
(S : AddSubmonoid M)
(oS : IsOpen ↑S)
:
theorem
Submonoid.mem_nhds_one
{M : Type u_3}
[TopologicalSpace M]
[CommMonoid M]
(S : Submonoid M)
(oS : IsOpen ↑S)
:
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)
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)
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))
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))
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
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
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
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
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
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
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
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
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
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
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)
:
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
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)
:
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
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
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
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
instance
instContinuousAddAdditiveOfContinuousMul
{M : Type u_3}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
Equations
- ⋯ = ⋯
instance
instContinuousMulMultiplicativeOfContinuousAdd
{M : Type u_3}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
Equations
- ⋯ = ⋯
theorem
continuousAdd_sInf
{M : Type u_3}
[Add M]
{ts : Set (TopologicalSpace M)}
(h : ∀ t ∈ ts, ContinuousAdd M)
:
theorem
continuousMul_sInf
{M : Type u_3}
[Mul M]
{ts : Set (TopologicalSpace M)}
(h : ∀ t ∈ ts, ContinuousMul M)
:
theorem
continuousAdd_iInf
{M : Type u_3}
{ι' : Sort u_6}
[Add M]
{ts : ι' → TopologicalSpace M}
(h' : ∀ (i : ι'), ContinuousAdd M)
:
theorem
continuousMul_iInf
{M : Type u_3}
{ι' : Sort u_6}
[Mul M]
{ts : ι' → TopologicalSpace M}
(h' : ∀ (i : ι'), ContinuousMul M)
:
theorem
continuousAdd_inf
{M : Type u_3}
[Add M]
{t₁ : TopologicalSpace M}
{t₂ : TopologicalSpace M}
(h₁ : ContinuousAdd M)
(h₂ : ContinuousAdd M)
:
theorem
continuousMul_inf
{M : Type u_3}
[Mul M]
{t₁ : TopologicalSpace M}
{t₂ : TopologicalSpace M}
(h₁ : ContinuousMul M)
(h₂ : ContinuousMul M)
:
The continuous map fun y => y + x
Equations
- ContinuousMap.addRight x = { toFun := fun (b : X) => b + x, continuous_toFun := ⋯ }
Instances For
The continuous map fun y => y * x
Equations
- ContinuousMap.mulRight x = { toFun := fun (b : X) => b * x, continuous_toFun := ⋯ }
Instances For
@[simp]
theorem
ContinuousMap.coe_addRight
{X : Type u_5}
[TopologicalSpace X]
[Add X]
[ContinuousAdd X]
(x : X)
:
⇑(ContinuousMap.addRight x) = fun (y : X) => y + x
@[simp]
theorem
ContinuousMap.coe_mulRight
{X : Type u_5}
[TopologicalSpace X]
[Mul X]
[ContinuousMul X]
(x : X)
:
⇑(ContinuousMap.mulRight x) = fun (y : X) => y * x
The continuous map fun y => x + y
Equations
- ContinuousMap.addLeft x = { toFun := fun (b : X) => x + b, continuous_toFun := ⋯ }
Instances For
The continuous map fun y => x * y
Equations
- ContinuousMap.mulLeft x = { toFun := fun (b : X) => x * b, continuous_toFun := ⋯ }
Instances For
@[simp]
theorem
ContinuousMap.coe_addLeft
{X : Type u_5}
[TopologicalSpace X]
[Add X]
[ContinuousAdd X]
(x : X)
:
⇑(ContinuousMap.addLeft x) = fun (y : X) => x + y
@[simp]
theorem
ContinuousMap.coe_mulLeft
{X : Type u_5}
[TopologicalSpace X]
[Mul X]
[ContinuousMul X]
(x : X)
:
⇑(ContinuousMap.mulLeft x) = fun (y : X) => x * y