Constructions of new uniform groups from old ones #
theorem
isUniformGroup_sInf
{G : Type u_1}
[Group G]
{us : Set (UniformSpace G)}
(h : ∀ u ∈ us, IsUniformGroup G)
:
theorem
isUniformAddGroup_sInf
{G : Type u_1}
[AddGroup G]
{us : Set (UniformSpace G)}
(h : ∀ u ∈ us, IsUniformAddGroup G)
:
@[deprecated isUniformAddGroup_sInf (since := "2025-03-31")]
theorem
uniformAddGroup_sInf
{G : Type u_1}
[AddGroup G]
{us : Set (UniformSpace G)}
(h : ∀ u ∈ us, IsUniformAddGroup G)
:
Alias of isUniformAddGroup_sInf.
@[deprecated isUniformGroup_sInf (since := "2025-03-31")]
theorem
uniformGroup_sInf
{G : Type u_1}
[Group G]
{us : Set (UniformSpace G)}
(h : ∀ u ∈ us, IsUniformGroup G)
:
Alias of isUniformGroup_sInf.
theorem
isUniformGroup_iInf
{G : Type u_1}
[Group G]
{ι : Sort u_4}
{us' : ι → UniformSpace G}
(h' : ∀ (i : ι), IsUniformGroup G)
:
theorem
isUniformAddGroup_iInf
{G : Type u_1}
[AddGroup G]
{ι : Sort u_4}
{us' : ι → UniformSpace G}
(h' : ∀ (i : ι), IsUniformAddGroup G)
:
@[deprecated isUniformAddGroup_iInf (since := "2025-03-31")]
theorem
uniformAddGroup_iInf
{G : Type u_1}
[AddGroup G]
{ι : Sort u_4}
{us' : ι → UniformSpace G}
(h' : ∀ (i : ι), IsUniformAddGroup G)
:
Alias of isUniformAddGroup_iInf.
@[deprecated isUniformGroup_iInf (since := "2025-03-31")]
theorem
uniformGroup_iInf
{G : Type u_1}
[Group G]
{ι : Sort u_4}
{us' : ι → UniformSpace G}
(h' : ∀ (i : ι), IsUniformGroup G)
:
Alias of isUniformGroup_iInf.
theorem
isUniformGroup_inf
{G : Type u_1}
[Group G]
{u₁ u₂ : UniformSpace G}
(h₁ : IsUniformGroup G)
(h₂ : IsUniformGroup G)
:
theorem
isUniformAddGroup_inf
{G : Type u_1}
[AddGroup G]
{u₁ u₂ : UniformSpace G}
(h₁ : IsUniformAddGroup G)
(h₂ : IsUniformAddGroup G)
:
@[deprecated isUniformAddGroup_inf (since := "2025-03-31")]
theorem
uniformAddGroup_inf
{G : Type u_1}
[AddGroup G]
{u₁ u₂ : UniformSpace G}
(h₁ : IsUniformAddGroup G)
(h₂ : IsUniformAddGroup G)
:
Alias of isUniformAddGroup_inf.
@[deprecated isUniformGroup_inf (since := "2025-03-31")]
theorem
uniformGroup_inf
{G : Type u_1}
[Group G]
{u₁ u₂ : UniformSpace G}
(h₁ : IsUniformGroup G)
(h₂ : IsUniformGroup G)
:
Alias of isUniformGroup_inf.
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)
:
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)
:
@[deprecated IsUniformInducing.isUniformAddGroup (since := "2025-03-30")]
theorem
IsUniformInducing.uniformAddGroup
{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)
:
Alias of IsUniformInducing.isUniformAddGroup.
@[deprecated IsUniformInducing.isUniformGroup (since := "2025-03-30")]
theorem
IsUniformInducing.uniformGroup
{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)
:
Alias of IsUniformInducing.isUniformGroup.
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)
:
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)
:
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)
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)
@[deprecated Prod.instIsUniformAddGroup (since := "2025-03-31")]
theorem
Prod.instUniformAddGroup
{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)
Alias of Prod.instIsUniformAddGroup.
@[deprecated Prod.instIsUniformGroup (since := "2025-03-31")]
theorem
Prod.instUniformGroup
{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)
Alias of Prod.instIsUniformGroup.
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)
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)
instance
instIsUniformGroupOfDiscreteUniformity
{G : Type u_1}
[Group G]
[UniformSpace G]
[DiscreteUniformity G]
:
The discrete uniformity makes a group a `IsUniformGroup.
instance
instIsUniformAddGroupOfDiscreteUniformity
{G : Type u_1}
[AddGroup G]
[UniformSpace G]
[DiscreteUniformity G]
:
The discrete uniformity makes an additive group a IsUniformAddGroup.