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
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[Zero M]
:
theorem
continuous_one
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[One M]
:
- continuous_add : Continuous fun p => p.fst + p.snd
Basic hypothesis to talk about a topological additive monoid or a topological additive
semigroup. A topological additive monoid over M, for example, is obtained by requiring both the
instances AddMonoid M and ContinuousAdd M.
Continuity in only the left/right argument can be stated using
ContinuousConstVAdd α α/ContinuousConstVAdd αᵐᵒᵖ α.
Instances
- continuous_mul : Continuous fun p => p.fst * p.snd
Basic hypothesis to talk about a topological monoid or a topological semigroup.
A topological monoid over M, for example, is obtained by requiring both the instances Monoid M
and ContinuousMul M.
Continuity in only the left/right argument can be stated using
ContinuousConstSMul α α/ContinuousConstSMul αᵐᵒᵖ α.
Instances
instance
instContinuousAddOrderDualInstTopologicalSpaceOrderDualInstAddOrderDual
{M : Type u_4}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
Equations
- (_ : ContinuousAdd Mᵒᵈ) = inst
instance
instContinuousMulOrderDualInstTopologicalSpaceOrderDualInstMulOrderDual
{M : Type u_4}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
Equations
- (_ : ContinuousMul Mᵒᵈ) = inst
theorem
continuous_add
{M : Type u_4}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
Continuous fun p => p.fst + p.snd
theorem
continuous_mul
{M : Type u_4}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
Continuous fun p => p.fst * p.snd
instance
ContinuousAdd.to_continuousVAdd
{M : Type u_4}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
ContinuousVAdd M M
theorem
ContinuousAdd.to_continuousVAdd.proof_1
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
ContinuousVAdd M M
instance
ContinuousMul.to_continuousSMul
{M : Type u_4}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
ContinuousSMul M M
theorem
ContinuousAdd.to_continuousVAdd_op.proof_1
{M : Type u_1}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
instance
ContinuousAdd.to_continuousVAdd_op
{M : Type u_4}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
instance
ContinuousMul.to_continuousSMul_op
{M : Type u_4}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
:
theorem
Continuous.add
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{f : X → M}
{g : X → M}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun x => f x + g x
theorem
Continuous.mul
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{f : X → M}
{g : X → M}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun x => f x * g x
theorem
continuous_add_left
{M : Type u_4}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
(a : M)
:
Continuous fun b => a + b
theorem
continuous_mul_left
{M : Type u_4}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
(a : M)
:
Continuous fun b => a * b
theorem
continuous_add_right
{M : Type u_4}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
(a : M)
:
Continuous fun b => b + a
theorem
continuous_mul_right
{M : Type u_4}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
(a : M)
:
Continuous fun b => b * a
theorem
ContinuousOn.add
{X : Type u_3}
{M : Type u_4}
[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 => f x + g x) s
theorem
ContinuousOn.mul
{X : Type u_3}
{M : Type u_4}
[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 => f x * g x) s
theorem
tendsto_add
{M : Type u_4}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
{a : M}
{b : M}
:
Filter.Tendsto (fun p => p.fst + p.snd) (nhds (a, b)) (nhds (a + b))
theorem
tendsto_mul
{M : Type u_4}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
{a : M}
{b : M}
:
Filter.Tendsto (fun p => p.fst * p.snd) (nhds (a, b)) (nhds (a * b))
theorem
Filter.Tendsto.add
{α : Type u_2}
{M : Type u_4}
[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_4}
[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_4}
[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_4}
[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_4}
[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_4}
[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
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₂))
:
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₂))
:
def
Filter.Tendsto.addUnits
{ι : Type u_1}
{N : Type u_5}
[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
Instances For
@[simp]
theorem
Filter.Tendsto.val_units
{ι : Type u_1}
{N : Type u_5}
[TopologicalSpace N]
[Monoid N]
[ContinuousMul N]
[T2Space N]
{f : ι → Nˣ}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[Filter.NeBot l]
(h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂))
:
↑(Filter.Tendsto.units h₁ h₂) = r₁
@[simp]
theorem
Filter.Tendsto.val_neg_addUnits
{ι : Type u_1}
{N : Type u_5}
[TopologicalSpace N]
[AddMonoid N]
[ContinuousAdd N]
[T2Space N]
{f : ι → AddUnits N}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[Filter.NeBot l]
(h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂))
:
↑(-Filter.Tendsto.addUnits h₁ h₂) = r₂
@[simp]
theorem
Filter.Tendsto.val_addUnits
{ι : Type u_1}
{N : Type u_5}
[TopologicalSpace N]
[AddMonoid N]
[ContinuousAdd N]
[T2Space N]
{f : ι → AddUnits N}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[Filter.NeBot l]
(h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂))
:
↑(Filter.Tendsto.addUnits h₁ h₂) = r₁
@[simp]
theorem
Filter.Tendsto.val_inv_units
{ι : Type u_1}
{N : Type u_5}
[TopologicalSpace N]
[Monoid N]
[ContinuousMul N]
[T2Space N]
{f : ι → Nˣ}
{r₁ : N}
{r₂ : N}
{l : Filter ι}
[Filter.NeBot l]
(h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁))
(h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂))
:
↑(Filter.Tendsto.units h₁ h₂)⁻¹ = r₂
def
Filter.Tendsto.units
{ι : Type u_1}
{N : Type u_5}
[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
Instances For
theorem
ContinuousAt.add
{X : Type u_3}
{M : Type u_4}
[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 => f x + g x) x
theorem
ContinuousAt.mul
{X : Type u_3}
{M : Type u_4}
[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 => f x * g x) x
theorem
ContinuousWithinAt.add
{X : Type u_3}
{M : Type u_4}
[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 => f x + g x) s x
theorem
ContinuousWithinAt.mul
{X : Type u_3}
{M : Type u_4}
[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 => f x * g x) s x
theorem
Prod.continuousAdd.proof_1
{M : Type u_1}
{N : Type u_2}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
[TopologicalSpace N]
[Add N]
[ContinuousAdd N]
:
ContinuousAdd (M × N)
instance
Prod.continuousAdd
{M : Type u_4}
{N : Type u_5}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
[TopologicalSpace N]
[Add N]
[ContinuousAdd N]
:
ContinuousAdd (M × N)
instance
Prod.continuousMul
{M : Type u_4}
{N : Type u_5}
[TopologicalSpace M]
[Mul M]
[ContinuousMul M]
[TopologicalSpace N]
[Mul N]
[ContinuousMul N]
:
ContinuousMul (M × N)
theorem
Pi.continuousAdd.proof_1
{ι : Type u_1}
{C : ι → Type u_2}
[(i : ι) → TopologicalSpace (C i)]
[(i : ι) → Add (C i)]
[∀ (i : ι), ContinuousAdd (C i)]
:
ContinuousAdd ((i : ι) → C i)
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
theorem
Pi.continuousAdd'.proof_1
{ι : Type u_1}
{M : Type u_2}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
ContinuousAdd (ι → M)
instance
Pi.continuousAdd'
{ι : Type u_1}
{M : Type u_4}
[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.
instance
Pi.continuousMul'
{ι : Type u_1}
{M : Type u_4}
[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.
instance
continuousAdd_of_discreteTopology
{N : Type u_5}
[TopologicalSpace N]
[Add N]
[DiscreteTopology N]
:
theorem
continuousAdd_of_discreteTopology.proof_1
{N : Type u_1}
[TopologicalSpace N]
[Add N]
[DiscreteTopology N]
:
instance
continuousMul_of_discreteTopology
{N : Type u_5}
[TopologicalSpace N]
[Mul N]
[DiscreteTopology N]
:
theorem
ContinuousAdd.of_nhds_zero
{M : Type u}
[AddMonoid M]
[TopologicalSpace M]
(hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0))
(hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0))
(hright : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => 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 => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1))
(hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1))
(hright : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => 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 => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0))
(hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => 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 => x * x_1) (nhds 1 ×ˢ nhds 1) (nhds 1))
(hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => 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₂]
:
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}
[AddMonoidHomClass F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (Set.range fun f x => ↑f x))
:
theorem
addMonoidHomOfMemClosureRangeCoe.proof_1
{M₁ : Type u_1}
{M₂ : Type u_2}
[TopologicalSpace M₂]
[T2Space M₂]
[AddZeroClass M₁]
[AddZeroClass M₂]
{F : Type u_3}
[AddMonoidHomClass F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (Set.range fun f x => ↑f x))
:
def
addMonoidHomOfMemClosureRangeCoe
{M₁ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace M₂]
[T2Space M₂]
[AddZeroClass M₁]
[AddZeroClass M₂]
[ContinuousAdd M₂]
{F : Type u_8}
[AddMonoidHomClass F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (Set.range fun f x => ↑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
- One or more equations did not get rendered due to their size.
Instances For
@[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}
[AddMonoidHomClass F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (Set.range fun f x => ↑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}
[MonoidHomClass F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (Set.range fun f x => ↑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}
[MonoidHomClass F M₁ M₂]
(f : M₁ → M₂)
(hf : f ∈ closure (Set.range fun f x => ↑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
- One or more equations did not get rendered due to their size.
Instances For
def
addMonoidHomOfTendsto
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace M₂]
[T2Space M₂]
[AddZeroClass M₁]
[AddZeroClass M₂]
[ContinuousAdd M₂]
{F : Type u_8}
[AddMonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[Filter.NeBot l]
(h : Filter.Tendsto (fun a x => ↑(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 (_ : f ∈ closure (Set.range fun f x => ↑f x))
Instances For
theorem
addMonoidHomOfTendsto.proof_1
{α : Type u_4}
{M₁ : Type u_1}
{M₂ : Type u_2}
[TopologicalSpace M₂]
[AddZeroClass M₁]
[AddZeroClass M₂]
{F : Type u_3}
[AddMonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[Filter.NeBot l]
(h : Filter.Tendsto (fun a x => ↑(g a) x) l (nhds f))
:
@[simp]
theorem
monoidHomOfTendsto_apply
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace M₂]
[T2Space M₂]
[MulOneClass M₁]
[MulOneClass M₂]
[ContinuousMul M₂]
{F : Type u_8}
[MonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[Filter.NeBot l]
(h : Filter.Tendsto (fun a x => ↑(g a) x) l (nhds f))
:
↑(monoidHomOfTendsto f g h) = f
@[simp]
theorem
addMonoidHomOfTendsto_apply
{α : Type u_2}
{M₁ : Type u_6}
{M₂ : Type u_7}
[TopologicalSpace M₂]
[T2Space M₂]
[AddZeroClass M₁]
[AddZeroClass M₂]
[ContinuousAdd M₂]
{F : Type u_8}
[AddMonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[Filter.NeBot l]
(h : Filter.Tendsto (fun a x => ↑(g a) x) l (nhds f))
:
↑(addMonoidHomOfTendsto 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}
[MonoidHomClass F M₁ M₂]
{l : Filter α}
(f : M₁ → M₂)
(g : α → F)
[Filter.NeBot l]
(h : Filter.Tendsto (fun a x => ↑(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 (_ : f ∈ closure (Set.range fun f x => ↑f x))
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]
[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]
[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]
[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]
[MulHomClass F M N]
[TopologicalSpace N]
[ContinuousMul N]
(f : F)
:
instance
AddSubsemigroup.continuousAdd
{M : Type u_4}
[TopologicalSpace M]
[AddSemigroup M]
[ContinuousAdd M]
(S : AddSubsemigroup M)
:
ContinuousAdd { x // x ∈ S }
theorem
AddSubsemigroup.continuousAdd.proof_1
{M : Type u_1}
[TopologicalSpace M]
[AddSemigroup M]
[ContinuousAdd M]
(S : AddSubsemigroup M)
:
ContinuousAdd { x // x ∈ S }
instance
Subsemigroup.continuousMul
{M : Type u_4}
[TopologicalSpace M]
[Semigroup M]
[ContinuousMul M]
(S : Subsemigroup M)
:
ContinuousMul { x // x ∈ S }
instance
AddSubmonoid.continuousAdd
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(S : AddSubmonoid M)
:
ContinuousAdd { x // x ∈ S }
theorem
AddSubmonoid.continuousAdd.proof_1
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(S : AddSubmonoid M)
:
ContinuousAdd { x // x ∈ S.toAddSubsemigroup }
instance
Submonoid.continuousMul
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(S : Submonoid M)
:
ContinuousMul { x // x ∈ S }
theorem
AddSubmonoid.top_closure_add_self_subset
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
theorem
Submonoid.top_closure_mul_self_subset
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
theorem
AddSubmonoid.top_closure_add_self_eq
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
theorem
Submonoid.top_closure_mul_self_eq
{M : Type u_4}
[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)
:
def
AddSubmonoid.topologicalClosure
{M : Type u_4}
[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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AddSubmonoid.topologicalClosure.proof_2
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
(s : AddSubmonoid M)
:
def
Submonoid.topologicalClosure
{M : Type u_4}
[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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AddSubmonoid.coe_topologicalClosure
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
↑(AddSubmonoid.topologicalClosure s) = closure ↑s
theorem
Submonoid.coe_topologicalClosure
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
↑(Submonoid.topologicalClosure s) = closure ↑s
theorem
AddSubmonoid.le_topologicalClosure
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
theorem
Submonoid.le_topologicalClosure
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
theorem
AddSubmonoid.isClosed_topologicalClosure
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
:
theorem
Submonoid.isClosed_topologicalClosure
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
:
theorem
AddSubmonoid.topologicalClosure_minimal
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
{t : AddSubmonoid M}
(h : s ≤ t)
(ht : IsClosed ↑t)
:
theorem
Submonoid.topologicalClosure_minimal
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(s : Submonoid M)
{t : Submonoid M}
(h : s ≤ t)
(ht : IsClosed ↑t)
:
abbrev
AddSubmonoid.addCommMonoidTopologicalClosure.match_1
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
(motive : { x // x ∈ AddSubmonoid.topologicalClosure s } → Prop)
:
(x : { x // x ∈ AddSubmonoid.topologicalClosure s }) →
((y : M) → (hy : y ∈ AddSubmonoid.topologicalClosure s) → motive { val := y, property := hy }) → motive x
Equations
- AddSubmonoid.addCommMonoidTopologicalClosure.match_1 s motive x h_1 = Subtype.casesOn x fun val property => h_1 val property
Instances For
theorem
AddSubmonoid.addCommMonoidTopologicalClosure.proof_4
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
(n : ℕ)
(x : { x // x ∈ AddSubmonoid.topologicalClosure s })
:
AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
theorem
AddSubmonoid.addCommMonoidTopologicalClosure.proof_5
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
[T2Space M]
(s : AddSubmonoid M)
(hs : ∀ (x y : { x // x ∈ s }), x + y = y + x)
:
∀ (x x_1 : { x // x ∈ AddSubmonoid.topologicalClosure s }), x + x_1 = x_1 + x
theorem
AddSubmonoid.addCommMonoidTopologicalClosure.proof_2
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
(a : { x // x ∈ AddSubmonoid.topologicalClosure s })
:
theorem
AddSubmonoid.addCommMonoidTopologicalClosure.proof_1
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
(a : { x // x ∈ AddSubmonoid.topologicalClosure s })
:
def
AddSubmonoid.addCommMonoidTopologicalClosure
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
[T2Space M]
(s : AddSubmonoid M)
(hs : ∀ (x y : { x // x ∈ s }), x + y = y + x)
:
AddCommMonoid { x // x ∈ AddSubmonoid.topologicalClosure s }
If a submonoid of an additive topological monoid is commutative, then so is its topological closure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AddSubmonoid.addCommMonoidTopologicalClosure.proof_3
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(s : AddSubmonoid M)
(x : { x // x ∈ AddSubmonoid.topologicalClosure s })
:
AddMonoid.nsmul 0 x = 0
def
Submonoid.commMonoidTopologicalClosure
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
[T2Space M]
(s : Submonoid M)
(hs : ∀ (x y : { x // x ∈ s }), x * y = y * x)
:
CommMonoid { x // x ∈ Submonoid.topologicalClosure s }
If a submonoid of a topological monoid is commutative, then so is its topological closure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
abbrev
exists_nhds_zero_half.match_1
{M : Type u_1}
[TopologicalSpace M]
[AddMonoid M]
{s : Set M}
(motive : (∃ V, IsOpen V ∧ 0 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v + w ∈ s) → Prop)
:
Equations
- exists_nhds_zero_half.match_1 motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => And.casesOn right fun left_1 right => h_1 w left left_1 right
Instances For
theorem
exists_open_nhds_zero_add_subset
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid 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_4}
[TopologicalSpace M]
[Monoid 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 VV ⊆ U.
theorem
IsCompact.add
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{s : Set M}
{t : Set M}
(hs : IsCompact s)
(ht : IsCompact t)
:
theorem
IsCompact.mul
{M : Type u_4}
[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_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : ι → α → M}
{x : Filter α}
{a : ι → M}
(l : List ι)
:
(∀ (i : ι), 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)))
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 : List ι) → (∀ (i : ι), i ∈ x → Filter.Tendsto (f i) x (nhds (a i))) → Prop)
:
(x : List ι) →
(x_1 : ∀ (i : ι), i ∈ x → Filter.Tendsto (f i) x (nhds (a i))) →
((x : ∀ (i : ι), i ∈ [] → Filter.Tendsto (f i) x (nhds (a i))) → motive [] x) →
((f : ι) → (l : List ι) → (h : ∀ (i : ι), i ∈ f :: l → Filter.Tendsto (f i) x (nhds (a i))) → motive (f :: l) h) →
motive x x_1
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
tendsto_list_prod
{ι : Type u_1}
{α : Type u_2}
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : ι → α → M}
{x : Filter α}
{a : ι → M}
(l : List ι)
:
(∀ (i : ι), 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)))
theorem
continuous_list_sum
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : ι → X → M}
(l : List ι)
(h : ∀ (i : ι), i ∈ l → Continuous (f i))
:
Continuous fun a => List.sum (List.map (fun i => f i a) l)
theorem
continuous_list_prod
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : ι → X → M}
(l : List ι)
(h : ∀ (i : ι), i ∈ l → Continuous (f i))
:
Continuous fun a => List.prod (List.map (fun i => f i a) l)
theorem
continuousOn_list_sum
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : ι → X → M}
(l : List ι)
{t : Set X}
(h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t)
:
ContinuousOn (fun a => List.sum (List.map (fun i => f i a) l)) t
theorem
continuousOn_list_prod
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : ι → X → M}
(l : List ι)
{t : Set X}
(h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t)
:
ContinuousOn (fun a => List.prod (List.map (fun i => f i a) l)) t
Equations
- continuous_nsmul.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n
Instances For
theorem
continuous_nsmul
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(n : ℕ)
:
Continuous fun a => n • a
theorem
continuous_pow
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(n : ℕ)
:
Continuous fun a => a ^ n
instance
AddMonoid.continuousConstSMul_nat
{A : Type u_6}
[AddMonoid A]
[TopologicalSpace A]
[ContinuousAdd A]
:
instance
AddMonoid.continuousSMul_nat
{A : Type u_6}
[AddMonoid A]
[TopologicalSpace A]
[ContinuousAdd A]
:
theorem
Continuous.nsmul
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : X → M}
(h : Continuous f)
(n : ℕ)
:
Continuous fun b => n • f b
theorem
Continuous.pow
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : X → M}
(h : Continuous f)
(n : ℕ)
:
Continuous fun b => f b ^ n
theorem
continuousOn_nsmul
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{s : Set M}
(n : ℕ)
:
ContinuousOn (fun x => n • x) s
theorem
continuousOn_pow
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{s : Set M}
(n : ℕ)
:
ContinuousOn (fun x => x ^ n) s
theorem
continuousAt_nsmul
{M : Type u_4}
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
(x : M)
(n : ℕ)
:
ContinuousAt (fun x => n • x) x
theorem
continuousAt_pow
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
(x : M)
(n : ℕ)
:
ContinuousAt (fun x => x ^ n) x
theorem
Filter.Tendsto.nsmul
{α : Type u_2}
{M : Type u_4}
[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_4}
[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
{X : Type u_3}
{M : Type u_4}
[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 => n • f x) s x
theorem
ContinuousWithinAt.pow
{X : Type u_3}
{M : Type u_4}
[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 => f x ^ n) s x
theorem
ContinuousAt.nsmul
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : X → M}
{x : X}
(hf : ContinuousAt f x)
(n : ℕ)
:
ContinuousAt (fun x => n • f x) x
theorem
ContinuousAt.pow
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : X → M}
{x : X}
(hf : ContinuousAt f x)
(n : ℕ)
:
ContinuousAt (fun x => f x ^ n) x
theorem
ContinuousOn.nsmul
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddMonoid M]
[ContinuousAdd M]
{f : X → M}
{s : Set X}
(hf : ContinuousOn f s)
(n : ℕ)
:
ContinuousOn (fun x => n • f x) s
theorem
ContinuousOn.pow
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{f : X → M}
{s : Set X}
(hf : ContinuousOn f s)
(n : ℕ)
:
ContinuousOn (fun x => f x ^ n) s
theorem
Filter.tendsto_cocompact_mul_left
{M : Type u_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{a : M}
{b : M}
(ha : b * a = 1)
:
Filter.Tendsto (fun x => 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_4}
[TopologicalSpace M]
[Monoid M]
[ContinuousMul M]
{a : M}
{b : M}
(ha : a * b = 1)
:
Filter.Tendsto (fun x => 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
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.
theorem
VAddAssocClass.continuousConstVAdd.proof_1
{R : Type u_1}
{A : Type u_2}
[AddMonoid A]
[VAdd R A]
[VAddAssocClass R A A]
[TopologicalSpace A]
[ContinuousAdd A]
:
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.
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ᵃᵒᵖ.
theorem
VAddCommClass.continuousConstVAdd.proof_1
{R : Type u_1}
{A : Type u_2}
[AddMonoid A]
[VAdd R A]
[VAddCommClass R A A]
[TopologicalSpace A]
[ContinuousAdd A]
:
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ᵐᵒᵖ.
theorem
AddOpposite.instContinuousAddAddOppositeInstTopologicalSpaceAddOppositeAdd.proof_1
{α : Type u_1}
[TopologicalSpace α]
[Add α]
[ContinuousAdd α]
:
instance
AddOpposite.instContinuousAddAddOppositeInstTopologicalSpaceAddOppositeAdd
{α : Type u_2}
[TopologicalSpace α]
[Add α]
[ContinuousAdd α]
:
If addition is continuous in α, then it also is in αᵃᵒᵖ.
instance
MulOpposite.instContinuousMulMulOppositeInstTopologicalSpaceMulOppositeMul
{α : Type u_2}
[TopologicalSpace α]
[Mul α]
[ContinuousMul α]
:
If multiplication is continuous in α, then it also is in αᵐᵒᵖ.
instance
AddUnits.instContinuousAddAddUnitsInstTopologicalSpaceAddUnitsToAddInstAddZeroClassAddUnits
{α : 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.
instance
Units.instContinuousMulUnitsInstTopologicalSpaceUnitsToMulInstMulOneClassUnits
{α : Type u_2}
[TopologicalSpace α]
[Monoid α]
[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.
theorem
Continuous.addUnits_map
{M : Type u_4}
{N : Type u_5}
[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_4}
{N : Type u_5}
[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_4}
[TopologicalSpace M]
[AddCommMonoid M]
(S : AddSubmonoid M)
(oS : IsOpen ↑S)
:
theorem
Submonoid.mem_nhds_one
{M : Type u_4}
[TopologicalSpace M]
[CommMonoid M]
(S : Submonoid M)
(oS : IsOpen ↑S)
:
theorem
tendsto_multiset_sum
{ι : Type u_1}
{α : Type u_2}
{M : Type u_4}
[TopologicalSpace M]
[AddCommMonoid M]
[ContinuousAdd M]
{f : ι → α → M}
{x : Filter α}
{a : ι → M}
(s : Multiset ι)
:
(∀ (i : ι), 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)))
theorem
tendsto_multiset_prod
{ι : Type u_1}
{α : Type u_2}
{M : Type u_4}
[TopologicalSpace M]
[CommMonoid M]
[ContinuousMul M]
{f : ι → α → M}
{x : Filter α}
{a : ι → M}
(s : Multiset ι)
:
(∀ (i : ι), 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)))
theorem
tendsto_finset_sum
{ι : Type u_1}
{α : Type u_2}
{M : Type u_4}
[TopologicalSpace M]
[AddCommMonoid M]
[ContinuousAdd M]
{f : ι → α → M}
{x : Filter α}
{a : ι → M}
(s : Finset ι)
:
(∀ (i : ι), 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))
theorem
tendsto_finset_prod
{ι : Type u_1}
{α : Type u_2}
{M : Type u_4}
[TopologicalSpace M]
[CommMonoid M]
[ContinuousMul M]
{f : ι → α → M}
{x : Filter α}
{a : ι → M}
(s : Finset ι)
:
(∀ (i : ι), 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))
theorem
continuous_multiset_sum
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddCommMonoid M]
[ContinuousAdd M]
{f : ι → X → M}
(s : Multiset ι)
:
(∀ (i : ι), i ∈ s → Continuous (f i)) → Continuous fun a => Multiset.sum (Multiset.map (fun i => f i a) s)
theorem
continuous_multiset_prod
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[CommMonoid M]
[ContinuousMul M]
{f : ι → X → M}
(s : Multiset ι)
:
(∀ (i : ι), i ∈ s → Continuous (f i)) → Continuous fun a => Multiset.prod (Multiset.map (fun i => f i a) s)
theorem
continuousOn_multiset_sum
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddCommMonoid M]
[ContinuousAdd M]
{f : ι → X → M}
(s : Multiset ι)
{t : Set X}
:
(∀ (i : ι), i ∈ s → ContinuousOn (f i) t) → ContinuousOn (fun a => Multiset.sum (Multiset.map (fun i => f i a) s)) t
theorem
continuousOn_multiset_prod
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[CommMonoid M]
[ContinuousMul M]
{f : ι → X → M}
(s : Multiset ι)
{t : Set X}
:
(∀ (i : ι), i ∈ s → ContinuousOn (f i) t) → ContinuousOn (fun a => Multiset.prod (Multiset.map (fun i => f i a) s)) t
theorem
continuous_finset_sum
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddCommMonoid M]
[ContinuousAdd M]
{f : ι → X → M}
(s : Finset ι)
:
(∀ (i : ι), i ∈ s → Continuous (f i)) → Continuous fun a => Finset.sum s fun i => f i a
theorem
continuous_finset_prod
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[CommMonoid M]
[ContinuousMul M]
{f : ι → X → M}
(s : Finset ι)
:
(∀ (i : ι), i ∈ s → Continuous (f i)) → Continuous fun a => Finset.prod s fun i => f i a
theorem
continuousOn_finset_sum
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[AddCommMonoid M]
[ContinuousAdd M]
{f : ι → X → M}
(s : Finset ι)
{t : Set X}
:
(∀ (i : ι), i ∈ s → ContinuousOn (f i) t) → ContinuousOn (fun a => Finset.sum s fun i => f i a) t
theorem
continuousOn_finset_prod
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[TopologicalSpace X]
[TopologicalSpace M]
[CommMonoid M]
[ContinuousMul M]
{f : ι → X → M}
(s : Finset ι)
{t : Set X}
:
(∀ (i : ι), i ∈ s → ContinuousOn (f i) t) → ContinuousOn (fun a => Finset.prod s fun i => f i a) t
theorem
eventuallyEq_sum
{ι : Type u_1}
{X : Type u_6}
{M : Type u_7}
[AddCommMonoid M]
{s : Finset ι}
{l : Filter X}
{f : ι → X → M}
{g : ι → X → M}
(hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i)
:
(Finset.sum s fun i => f i) =ᶠ[l] Finset.sum s fun i => g i
theorem
eventuallyEq_prod
{ι : Type u_1}
{X : Type u_6}
{M : Type u_7}
[CommMonoid M]
{s : Finset ι}
{l : Filter X}
{f : ι → X → M}
{g : ι → X → M}
(hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i)
:
(Finset.prod s fun i => f i) =ᶠ[l] Finset.prod s fun i => g i
theorem
LocallyFinite.exists_finset_support
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{M : Type u_6}
[AddCommMonoid M]
{f : ι → X → M}
(hf : LocallyFinite fun i => Function.support (f i))
(x₀ : X)
:
∃ I, ∀ᶠ (x : X) in nhds x₀, (Function.support fun i => f i x) ⊆ ↑I
theorem
LocallyFinite.exists_finset_mulSupport
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{M : Type u_6}
[CommMonoid M]
{f : ι → X → M}
(hf : LocallyFinite fun i => Function.mulSupport (f i))
(x₀ : X)
:
∃ I, ∀ᶠ (x : X) in nhds x₀, (Function.mulSupport fun i => f i x) ⊆ ↑I
theorem
finsum_eventually_eq_sum
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{M : Type u_6}
[AddCommMonoid M]
{f : ι → X → M}
(hf : LocallyFinite fun i => Function.support (f i))
(x : X)
:
∃ s, ∀ᶠ (y : X) in nhds x, ∑ᶠ (i : ι), f i y = Finset.sum s fun i => f i y
abbrev
finsum_eventually_eq_sum.match_1
{ι : Type u_1}
{X : Type u_2}
[TopologicalSpace X]
{M : Type u_3}
[AddCommMonoid M]
{f : ι → X → M}
(x : X)
(motive : (∃ I, ∀ᶠ (x : X) in nhds x, (Function.support fun i => f i x) ⊆ ↑I) → Prop)
:
(x : ∃ I, ∀ᶠ (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 (_ : ∃ I, ∀ᶠ (x : X) in nhds x, (Function.support fun i => f i x) ⊆ ↑I)) →
motive x
Equations
- finsum_eventually_eq_sum.match_1 x motive x h_1 = Exists.casesOn x fun w h => h_1 w h
Instances For
theorem
finprod_eventually_eq_prod
{ι : Type u_1}
{X : Type u_3}
[TopologicalSpace X]
{M : Type u_6}
[CommMonoid M]
{f : ι → X → M}
(hf : LocallyFinite fun i => Function.mulSupport (f i))
(x : X)
:
∃ s, ∀ᶠ (y : X) in nhds x, ∏ᶠ (i : ι), f i y = Finset.prod s fun i => f i y
theorem
continuous_finsum
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[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 => ∑ᶠ (i : ι), f i x
theorem
continuous_finprod
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[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 => ∏ᶠ (i : ι), f i x
theorem
continuous_finsum_cond
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[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 => ∑ᶠ (i : ι) (x_1 : p i), f i x
theorem
continuous_finprod_cond
{ι : Type u_1}
{X : Type u_3}
{M : Type u_4}
[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 => ∏ᶠ (i : ι) (x_1 : p i), f i x
instance
instContinuousMulMultiplicativeInstTopologicalSpaceMultiplicativeMul
{M : Type u_4}
[TopologicalSpace M]
[Add M]
[ContinuousAdd M]
:
theorem
continuousAdd_sInf
{M : Type u_4}
[Add M]
{ts : Set (TopologicalSpace M)}
(h : ∀ (t : TopologicalSpace M), t ∈ ts → ContinuousAdd M)
:
theorem
continuousMul_sInf
{M : Type u_4}
[Mul M]
{ts : Set (TopologicalSpace M)}
(h : ∀ (t : TopologicalSpace M), t ∈ ts → ContinuousMul M)
:
theorem
continuousAdd_iInf
{M : Type u_4}
{ι' : Sort u_6}
[Add M]
{ts : ι' → TopologicalSpace M}
(h' : ∀ (i : ι'), ContinuousAdd M)
:
theorem
continuousMul_iInf
{M : Type u_4}
{ι' : Sort u_6}
[Mul M]
{ts : ι' → TopologicalSpace M}
(h' : ∀ (i : ι'), ContinuousMul M)
:
theorem
continuousAdd_inf
{M : Type u_4}
[Add M]
{t₁ : TopologicalSpace M}
{t₂ : TopologicalSpace M}
(h₁ : ContinuousAdd M)
(h₂ : ContinuousAdd M)
:
theorem
continuousMul_inf
{M : Type u_4}
[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 = ContinuousMap.mk fun b => b + x
Instances For
The continuous map fun y => y * x
Equations
- ContinuousMap.mulRight x = ContinuousMap.mk fun b => b * x
Instances For
@[simp]
theorem
ContinuousMap.coe_addRight
{X : Type u_3}
[TopologicalSpace X]
[Add X]
[ContinuousAdd X]
(x : X)
:
↑(ContinuousMap.addRight x) = fun y => y + x
@[simp]
theorem
ContinuousMap.coe_mulRight
{X : Type u_3}
[TopologicalSpace X]
[Mul X]
[ContinuousMul X]
(x : X)
:
↑(ContinuousMap.mulRight x) = fun y => y * x
The continuous map fun y => x + y
Equations
- ContinuousMap.addLeft x = ContinuousMap.mk fun b => x + b
Instances For
The continuous map fun y => x * y
Equations
- ContinuousMap.mulLeft x = ContinuousMap.mk fun b => x * b
Instances For
@[simp]
theorem
ContinuousMap.coe_addLeft
{X : Type u_3}
[TopologicalSpace X]
[Add X]
[ContinuousAdd X]
(x : X)
:
↑(ContinuousMap.addLeft x) = fun y => x + y
@[simp]
theorem
ContinuousMap.coe_mulLeft
{X : Type u_3}
[TopologicalSpace X]
[Mul X]
[ContinuousMul X]
(x : X)
:
↑(ContinuousMap.mulLeft x) = fun y => x * y