# Constructions of new uniform groups from old ones #

source
theorem isUniformGroup_sInf {G : Type u_1} [Group G] {us : Set (UniformSpace G)} (h : ∀ u ∈ us, IsUniformGroup G) :
IsUniformGroup G
source
theorem isUniformAddGroup_sInf {G : Type u_1} [AddGroup G] {us : Set (UniformSpace G)} (h : ∀ u ∈ us, IsUniformAddGroup G) :
IsUniformAddGroup G
source
theorem isUniformGroup_iInf {G : Type u_1} [Group G] {ι : Sort u_4} {us' : ι → UniformSpace G} (h' : ∀ (i : ι), IsUniformGroup G) :
IsUniformGroup G
source
theorem isUniformAddGroup_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_4} {us' : ι → UniformSpace G} (h' : ∀ (i : ι), IsUniformAddGroup G) :
IsUniformAddGroup G
source
theorem isUniformGroup_inf {G : Type u_1} [Group G] {u₁ u₂ : UniformSpace G} (h₁ : IsUniformGroup G) (h₂ : IsUniformGroup G) :
IsUniformGroup G
source
theorem isUniformAddGroup_inf {G : Type u_1} [AddGroup G] {u₁ u₂ : UniformSpace G} (h₁ : IsUniformAddGroup G) (h₂ : IsUniformAddGroup G) :
IsUniformAddGroup G
source
theorem IsUniformInducing.isUniformGroup {G : Type u_1} {H : Type u_2} {hom : Type u_3} [Group G] [Group H] [UniformSpace G] [UniformSpace H] [IsUniformGroup H] [FunLike hom G H] [MonoidHomClass hom G H] (f : hom) (hf : IsUniformInducing ⇑f) :
IsUniformGroup G
source
theorem IsUniformInducing.isUniformAddGroup {G : Type u_1} {H : Type u_2} {hom : Type u_3} [AddGroup G] [AddGroup H] [UniformSpace G] [UniformSpace H] [IsUniformAddGroup H] [FunLike hom G H] [AddMonoidHomClass hom G H] (f : hom) (hf : IsUniformInducing ⇑f) :
IsUniformAddGroup G
source
theorem IsUniformGroup.comap {G : Type u_1} {H : Type u_2} {hom : Type u_3} [Group G] [Group H] {u : UniformSpace H} [IsUniformGroup H] [FunLike hom G H] [MonoidHomClass hom G H] (f : hom) :
IsUniformGroup G
source
theorem IsUniformAddGroup.comap {G : Type u_1} {H : Type u_2} {hom : Type u_3} [AddGroup G] [AddGroup H] {u : UniformSpace H} [IsUniformAddGroup H] [FunLike hom G H] [AddMonoidHomClass hom G H] (f : hom) :
IsUniformAddGroup G
source
instance Prod.instIsUniformGroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] [UniformSpace G] [hG : IsUniformGroup G] [UniformSpace H] [hH : IsUniformGroup H] :
IsUniformGroup (G × H)
source
instance Prod.instIsUniformAddGroup {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [UniformSpace G] [hG : IsUniformAddGroup G] [UniformSpace H] [hH : IsUniformAddGroup H] :
IsUniformAddGroup (G × H)
source
instance Pi.instIsUniformGroup {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → UniformSpace (G i)] [(i : ι) → Group (G i)] [∀ (i : ι), IsUniformGroup (G i)] :
IsUniformGroup ((i : ι) → G i)
source
instance Pi.instIsUniformAddGroup {ι : Type u_4} {G : ι → Type u_5} [(i : ι) → UniformSpace (G i)] [(i : ι) → AddGroup (G i)] [∀ (i : ι), IsUniformAddGroup (G i)] :
IsUniformAddGroup ((i : ι) → G i)
source
instance instIsUniformGroupOfDiscreteUniformity {G : Type u_1} [Group G] [UniformSpace G] [DiscreteUniformity G] :
IsUniformGroup G

The discrete uniformity makes a group a `IsUniformGroup.

source
instance instIsUniformAddGroupOfDiscreteUniformity {G : Type u_1} [AddGroup G] [UniformSpace G] [DiscreteUniformity G] :
IsUniformAddGroup G

The discrete uniformity makes an additive group a `IsUniformAddGroup`.