Uniform structure on topological groups #
This file defines uniform groups and its additive counterpart. These typeclasses should be
preferred over using [TopologicalSpace α] [TopologicalGroup α] since every topological
group naturally induces a uniform structure.
Main declarations #
UniformGroupandUniformAddGroup: Multiplicative and additive uniform groups, i.e., groups with uniformly continuous(*)and(⁻¹)/(+)and(-).
Main results #
TopologicalAddGroup.toUniformSpaceandcomm_topologicalAddGroup_is_uniformcan be used to construct a canonical uniformity for a topological add group.
See Mathlib.Topology.Algebra.UniformGroup.Basic for further results.
A uniform group is a group in which multiplication and inversion are uniformly continuous.
- uniformContinuous_div : UniformContinuous fun (p : α × α) => p.1 / p.2
Instances
A uniform additive group is an additive group in which addition and negation are uniformly continuous.
- uniformContinuous_sub : UniformContinuous fun (p : α × α) => p.1 - p.2
Instances
theorem
UniformGroup.mk'
{α : Type u_3}
[UniformSpace α]
[Group α]
(h₁ : UniformContinuous fun (p : α × α) => p.1 * p.2)
(h₂ : UniformContinuous fun (p : α) => p⁻¹)
:
theorem
UniformAddGroup.mk'
{α : Type u_3}
[UniformSpace α]
[AddGroup α]
(h₁ : UniformContinuous fun (p : α × α) => p.1 + p.2)
(h₂ : UniformContinuous fun (p : α) => -p)
:
theorem
uniformContinuous_div
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
:
UniformContinuous fun (p : α × α) => p.1 / p.2
theorem
uniformContinuous_sub
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
UniformContinuous fun (p : α × α) => p.1 - p.2
theorem
UniformContinuous.div
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
{f g : β → α}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
:
UniformContinuous fun (x : β) => f x / g x
theorem
UniformContinuous.sub
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
{f g : β → α}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
:
UniformContinuous fun (x : β) => f x - g x
theorem
UniformContinuous.inv
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
:
UniformContinuous fun (x : β) => (f x)⁻¹
theorem
UniformContinuous.neg
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
:
UniformContinuous fun (x : β) => -f x
theorem
uniformContinuous_inv
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
:
UniformContinuous fun (x : α) => x⁻¹
theorem
uniformContinuous_neg
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
UniformContinuous fun (x : α) => -x
theorem
UniformContinuous.mul
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
{f g : β → α}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
:
UniformContinuous fun (x : β) => f x * g x
theorem
UniformContinuous.add
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
{f g : β → α}
(hf : UniformContinuous f)
(hg : UniformContinuous g)
:
UniformContinuous fun (x : β) => f x + g x
theorem
uniformContinuous_mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
:
UniformContinuous fun (p : α × α) => p.1 * p.2
theorem
uniformContinuous_add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
UniformContinuous fun (p : α × α) => p.1 + p.2
theorem
UniformContinuous.mul_const
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(a : α)
:
UniformContinuous fun (x : β) => f x * a
theorem
UniformContinuous.add_const
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(a : α)
:
UniformContinuous fun (x : β) => f x + a
theorem
UniformContinuous.const_mul
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(a : α)
:
UniformContinuous fun (x : β) => a * f x
theorem
UniformContinuous.const_add
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(a : α)
:
UniformContinuous fun (x : β) => a + f x
theorem
uniformContinuous_mul_left
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(a : α)
:
UniformContinuous fun (b : α) => a * b
theorem
uniformContinuous_add_left
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
(a : α)
:
UniformContinuous fun (b : α) => a + b
theorem
uniformContinuous_mul_right
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(a : α)
:
UniformContinuous fun (b : α) => b * a
theorem
uniformContinuous_add_right
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
(a : α)
:
UniformContinuous fun (b : α) => b + a
theorem
UniformContinuous.div_const
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(a : α)
:
UniformContinuous fun (x : β) => f x / a
theorem
UniformContinuous.sub_const
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(a : α)
:
UniformContinuous fun (x : β) => f x - a
theorem
uniformContinuous_div_const
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(a : α)
:
UniformContinuous fun (b : α) => b / a
theorem
uniformContinuous_sub_const
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
(a : α)
:
UniformContinuous fun (b : α) => b - a
theorem
UniformContinuous.pow_const
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(n : ℕ)
:
UniformContinuous fun (x : β) => f x ^ n
theorem
UniformContinuous.const_nsmul
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(n : ℕ)
:
UniformContinuous fun (x : β) => n • f x
theorem
uniformContinuous_pow_const
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(n : ℕ)
:
UniformContinuous fun (x : α) => x ^ n
theorem
uniformContinuous_const_nsmul
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
(n : ℕ)
:
UniformContinuous fun (x : α) => n • x
theorem
UniformContinuous.zpow_const
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(n : ℤ)
:
UniformContinuous fun (x : β) => f x ^ n
theorem
UniformContinuous.const_zsmul
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
{f : β → α}
(hf : UniformContinuous f)
(n : ℤ)
:
UniformContinuous fun (x : β) => n • f x
theorem
uniformContinuous_zpow_const
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(n : ℤ)
:
UniformContinuous fun (x : α) => x ^ n
theorem
uniformContinuous_const_zsmul
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
(n : ℤ)
:
UniformContinuous fun (x : α) => n • x
@[instance 10]
instance
UniformGroup.to_topologicalGroup
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
:
@[instance 10]
instance
UniformAddGroup.to_topologicalAddGroup
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
instance
instUniformGroupProd
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
[Group β]
[UniformGroup β]
:
UniformGroup (α × β)
instance
instUniformAddGroupSum
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
[AddGroup β]
[UniformAddGroup β]
:
UniformAddGroup (α × β)
theorem
uniformity_translate_mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
(a : α)
:
Filter.map (fun (x : α × α) => (x.1 * a, x.2 * a)) (uniformity α) = uniformity α
theorem
uniformity_translate_add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
(a : α)
:
Filter.map (fun (x : α × α) => (x.1 + a, x.2 + a)) (uniformity α) = uniformity α
instance
AddOpposite.instUniformAddGroup
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
theorem
uniformGroup_sInf
{β : Type u_2}
[Group β]
{us : Set (UniformSpace β)}
(h : ∀ u ∈ us, UniformGroup β)
:
theorem
uniformAddGroup_sInf
{β : Type u_2}
[AddGroup β]
{us : Set (UniformSpace β)}
(h : ∀ u ∈ us, UniformAddGroup β)
:
theorem
uniformGroup_iInf
{β : Type u_2}
[Group β]
{ι : Sort u_3}
{us' : ι → UniformSpace β}
(h' : ∀ (i : ι), UniformGroup β)
:
theorem
uniformAddGroup_iInf
{β : Type u_2}
[AddGroup β]
{ι : Sort u_3}
{us' : ι → UniformSpace β}
(h' : ∀ (i : ι), UniformAddGroup β)
:
theorem
uniformGroup_inf
{β : Type u_2}
[Group β]
{u₁ u₂ : UniformSpace β}
(h₁ : UniformGroup β)
(h₂ : UniformGroup β)
:
theorem
uniformAddGroup_inf
{β : Type u_2}
[AddGroup β]
{u₁ u₂ : UniformSpace β}
(h₁ : UniformAddGroup β)
(h₂ : UniformAddGroup β)
:
theorem
uniformity_eq_comap_nhds_one
(α : Type u_1)
[UniformSpace α]
[Group α]
[UniformGroup α]
:
uniformity α = Filter.comap (fun (x : α × α) => x.2 / x.1) (nhds 1)
theorem
uniformity_eq_comap_nhds_zero
(α : Type u_1)
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
uniformity α = Filter.comap (fun (x : α × α) => x.2 - x.1) (nhds 0)
theorem
uniformity_eq_comap_nhds_one_swapped
(α : Type u_1)
[UniformSpace α]
[Group α]
[UniformGroup α]
:
uniformity α = Filter.comap (fun (x : α × α) => x.1 / x.2) (nhds 1)
theorem
uniformity_eq_comap_nhds_zero_swapped
(α : Type u_1)
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
uniformity α = Filter.comap (fun (x : α × α) => x.1 - x.2) (nhds 0)
theorem
UniformGroup.ext
{G : Type u_3}
[Group G]
{u v : UniformSpace G}
(hu : UniformGroup G)
(hv : UniformGroup G)
(h : nhds 1 = nhds 1)
:
u = v
theorem
UniformAddGroup.ext
{G : Type u_3}
[AddGroup G]
{u v : UniformSpace G}
(hu : UniformAddGroup G)
(hv : UniformAddGroup G)
(h : nhds 0 = nhds 0)
:
u = v
theorem
UniformGroup.ext_iff
{G : Type u_3}
[Group G]
{u v : UniformSpace G}
(hu : UniformGroup G)
(hv : UniformGroup G)
:
theorem
UniformAddGroup.ext_iff
{G : Type u_3}
[AddGroup G]
{u v : UniformSpace G}
(hu : UniformAddGroup G)
(hv : UniformAddGroup G)
:
theorem
UniformGroup.uniformity_countably_generated
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
[(nhds 1).IsCountablyGenerated]
:
(uniformity α).IsCountablyGenerated
theorem
UniformAddGroup.uniformity_countably_generated
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[(nhds 0).IsCountablyGenerated]
:
(uniformity α).IsCountablyGenerated
theorem
uniformity_eq_comap_inv_mul_nhds_one
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
:
uniformity α = Filter.comap (fun (x : α × α) => x.1⁻¹ * x.2) (nhds 1)
theorem
uniformity_eq_comap_neg_add_nhds_zero
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
uniformity α = Filter.comap (fun (x : α × α) => -x.1 + x.2) (nhds 0)
theorem
uniformity_eq_comap_inv_mul_nhds_one_swapped
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
:
uniformity α = Filter.comap (fun (x : α × α) => x.2⁻¹ * x.1) (nhds 1)
theorem
uniformity_eq_comap_neg_add_nhds_zero_swapped
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
:
uniformity α = Filter.comap (fun (x : α × α) => -x.2 + x.1) (nhds 0)
theorem
Filter.HasBasis.uniformity_of_nhds_one
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{ι : Sort u_3}
{p : ι → Prop}
{U : ι → Set α}
(h : (nhds 1).HasBasis p U)
:
(uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.2 / x.1 ∈ U i}
theorem
Filter.HasBasis.uniformity_of_nhds_zero
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{ι : Sort u_3}
{p : ι → Prop}
{U : ι → Set α}
(h : (nhds 0).HasBasis p U)
:
(uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.2 - x.1 ∈ U i}
theorem
Filter.HasBasis.uniformity_of_nhds_one_inv_mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{ι : Sort u_3}
{p : ι → Prop}
{U : ι → Set α}
(h : (nhds 1).HasBasis p U)
:
(uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.1⁻¹ * x.2 ∈ U i}
theorem
Filter.HasBasis.uniformity_of_nhds_zero_neg_add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{ι : Sort u_3}
{p : ι → Prop}
{U : ι → Set α}
(h : (nhds 0).HasBasis p U)
:
(uniformity α).HasBasis p fun (i : ι) => {x : α × α | -x.1 + x.2 ∈ U i}
theorem
Filter.HasBasis.uniformity_of_nhds_one_swapped
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{ι : Sort u_3}
{p : ι → Prop}
{U : ι → Set α}
(h : (nhds 1).HasBasis p U)
:
(uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.1 / x.2 ∈ U i}
theorem
Filter.HasBasis.uniformity_of_nhds_zero_swapped
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{ι : Sort u_3}
{p : ι → Prop}
{U : ι → Set α}
(h : (nhds 0).HasBasis p U)
:
(uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.1 - x.2 ∈ U i}
theorem
Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped
{α : Type u_1}
[UniformSpace α]
[Group α]
[UniformGroup α]
{ι : Sort u_3}
{p : ι → Prop}
{U : ι → Set α}
(h : (nhds 1).HasBasis p U)
:
(uniformity α).HasBasis p fun (i : ι) => {x : α × α | x.2⁻¹ * x.1 ∈ U i}
theorem
Filter.HasBasis.uniformity_of_nhds_zero_neg_add_swapped
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{ι : Sort u_3}
{p : ι → Prop}
{U : ι → Set α}
(h : (nhds 0).HasBasis p U)
:
(uniformity α).HasBasis p fun (i : ι) => {x : α × α | -x.2 + x.1 ∈ U i}
theorem
uniformContinuous_of_tendsto_one
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
{hom : Type u_3}
[UniformSpace β]
[Group β]
[UniformGroup β]
[FunLike hom α β]
[MonoidHomClass hom α β]
{f : hom}
(h : Filter.Tendsto (⇑f) (nhds 1) (nhds 1))
:
theorem
uniformContinuous_of_tendsto_zero
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{hom : Type u_3}
[UniformSpace β]
[AddGroup β]
[UniformAddGroup β]
[FunLike hom α β]
[AddMonoidHomClass hom α β]
{f : hom}
(h : Filter.Tendsto (⇑f) (nhds 0) (nhds 0))
:
theorem
uniformContinuous_of_continuousAt_one
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
{hom : Type u_3}
[UniformSpace β]
[Group β]
[UniformGroup β]
[FunLike hom α β]
[MonoidHomClass hom α β]
(f : hom)
(hf : ContinuousAt (⇑f) 1)
:
A group homomorphism (a bundled morphism of a type that implements MonoidHomClass) between
two uniform groups is uniformly continuous provided that it is continuous at one. See also
continuous_of_continuousAt_one.
theorem
uniformContinuous_of_continuousAt_zero
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{hom : Type u_3}
[UniformSpace β]
[AddGroup β]
[UniformAddGroup β]
[FunLike hom α β]
[AddMonoidHomClass hom α β]
(f : hom)
(hf : ContinuousAt (⇑f) 0)
:
An additive group homomorphism (a bundled morphism of a type that implements
AddMonoidHomClass) between two uniform additive groups is uniformly continuous provided that it
is continuous at zero. See also continuous_of_continuousAt_zero.
theorem
MonoidHom.uniformContinuous_of_continuousAt_one
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
[UniformSpace β]
[Group β]
[UniformGroup β]
(f : α →* β)
(hf : ContinuousAt (⇑f) 1)
:
theorem
AddMonoidHom.uniformContinuous_of_continuousAt_zero
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
[UniformSpace β]
[AddGroup β]
[UniformAddGroup β]
(f : α →+ β)
(hf : ContinuousAt (⇑f) 0)
:
theorem
UniformGroup.uniformContinuous_iff_isOpen_ker
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
{hom : Type u_3}
[UniformSpace β]
[DiscreteTopology β]
[Group β]
[UniformGroup β]
[FunLike hom α β]
[MonoidHomClass hom α β]
{f : hom}
:
UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
A homomorphism from a uniform group to a discrete uniform group is continuous if and only if its kernel is open.
theorem
UniformAddGroup.uniformContinuous_iff_isOpen_ker
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{hom : Type u_3}
[UniformSpace β]
[DiscreteTopology β]
[AddGroup β]
[UniformAddGroup β]
[FunLike hom α β]
[AddMonoidHomClass hom α β]
{f : hom}
:
UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
A homomorphism from a uniform additive group to a discrete uniform additive group is continuous if and only if its kernel is open.
@[deprecated UniformGroup.uniformContinuous_iff_isOpen_ker]
theorem
UniformGroup.uniformContinuous_iff_open_ker
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
{hom : Type u_3}
[UniformSpace β]
[DiscreteTopology β]
[Group β]
[UniformGroup β]
[FunLike hom α β]
[MonoidHomClass hom α β]
{f : hom}
:
UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
Alias of UniformGroup.uniformContinuous_iff_isOpen_ker.
A homomorphism from a uniform group to a discrete uniform group is continuous if and only if its kernel is open.
@[deprecated UniformAddGroup.uniformContinuous_iff_isOpen_ker]
theorem
UniformAddGroup.uniformContinuous_iff_open_ker
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{hom : Type u_3}
[UniformSpace β]
[DiscreteTopology β]
[AddGroup β]
[UniformAddGroup β]
[FunLike hom α β]
[AddMonoidHomClass hom α β]
{f : hom}
:
UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
Alias of UniformAddGroup.uniformContinuous_iff_isOpen_ker.
A homomorphism from a uniform additive group to a discrete uniform additive group is continuous if and only if its kernel is open.
theorem
uniformContinuous_monoidHom_of_continuous
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[UniformGroup α]
{hom : Type u_3}
[UniformSpace β]
[Group β]
[UniformGroup β]
[FunLike hom α β]
[MonoidHomClass hom α β]
{f : hom}
(h : Continuous ⇑f)
:
theorem
uniformContinuous_addMonoidHom_of_continuous
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[UniformAddGroup α]
{hom : Type u_3}
[UniformSpace β]
[AddGroup β]
[UniformAddGroup β]
[FunLike hom α β]
[AddMonoidHomClass hom α β]
{f : hom}
(h : Continuous ⇑f)
:
def
TopologicalGroup.toUniformSpace
(G : Type u_1)
[Group G]
[TopologicalSpace G]
[TopologicalGroup G]
:
The right uniformity on a topological group (as opposed to the left uniformity).
Warning: in general the right and left uniformities do not coincide and so one does not obtain a
UniformGroup structure. Two important special cases where they do coincide are for
commutative groups (see comm_topologicalGroup_is_uniform) and for compact groups (see
topologicalGroup_is_uniform_of_compactSpace).
Equations
- TopologicalGroup.toUniformSpace G = UniformSpace.mk (Filter.comap (fun (p : G × G) => p.2 / p.1) (nhds 1)) ⋯ ⋯ ⋯
Instances For
def
TopologicalAddGroup.toUniformSpace
(G : Type u_1)
[AddGroup G]
[TopologicalSpace G]
[TopologicalAddGroup G]
:
The right uniformity on a topological additive group (as opposed to the left uniformity).
Warning: in general the right and left uniformities do not coincide and so one does not obtain a
UniformAddGroup structure. Two important special cases where they do coincide are for
commutative additive groups (see comm_topologicalAddGroup_is_uniform) and for compact
additive groups (see topologicalAddGroup_is_uniform_of_compactSpace).
Equations
- TopologicalAddGroup.toUniformSpace G = UniformSpace.mk (Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)) ⋯ ⋯ ⋯
Instances For
theorem
uniformity_eq_comap_nhds_one'
(G : Type u_1)
[Group G]
[TopologicalSpace G]
[TopologicalGroup G]
:
uniformity G = Filter.comap (fun (p : G × G) => p.2 / p.1) (nhds 1)
theorem
uniformity_eq_comap_nhds_zero'
(G : Type u_1)
[AddGroup G]
[TopologicalSpace G]
[TopologicalAddGroup G]
:
uniformity G = Filter.comap (fun (p : G × G) => p.2 - p.1) (nhds 0)
theorem
comm_topologicalGroup_is_uniform
{G : Type u_1}
[CommGroup G]
[TopologicalSpace G]
[TopologicalGroup G]
:
theorem
comm_topologicalAddGroup_is_uniform
{G : Type u_1}
[AddCommGroup G]
[TopologicalSpace G]
[TopologicalAddGroup G]
:
theorem
UniformGroup.toUniformSpace_eq
{G : Type u_2}
[u : UniformSpace G]
[Group G]
[UniformGroup G]
:
theorem
UniformAddGroup.toUniformSpace_eq
{G : Type u_2}
[u : UniformSpace G]
[AddGroup G]
[UniformAddGroup G]
:
theorem
tendsto_div_comap_self
{α : Type u_1}
{β : Type u_2}
{hom : Type u_3}
[TopologicalSpace α]
[Group α]
[TopologicalGroup α]
[TopologicalSpace β]
[Group β]
[FunLike hom β α]
[MonoidHomClass hom β α]
{e : hom}
(de : IsDenseInducing ⇑e)
(x₀ : α)
:
Filter.Tendsto (fun (t : β × β) => t.2 / t.1) (Filter.comap (fun (p : β × β) => (e p.1, e p.2)) (nhds (x₀, x₀)))
(nhds 1)
theorem
tendsto_sub_comap_self
{α : Type u_1}
{β : Type u_2}
{hom : Type u_3}
[TopologicalSpace α]
[AddGroup α]
[TopologicalAddGroup α]
[TopologicalSpace β]
[AddGroup β]
[FunLike hom β α]
[AddMonoidHomClass hom β α]
{e : hom}
(de : IsDenseInducing ⇑e)
(x₀ : α)
:
Filter.Tendsto (fun (t : β × β) => t.2 - t.1) (Filter.comap (fun (p : β × β) => (e p.1, e p.2)) (nhds (x₀, x₀)))
(nhds 0)