Uniform structure on topological groups

Main results

• extension of ℤ-bilinear maps to complete groups (useful for ring completions)

• QuotientGroup.completeSpace_left and QuotientAddGroup.completeSpace_left guarantee that quotients of first countable topological groups by normal subgroups are themselves complete, for the left uniformity. We also give versions for the right uniformity. In particular, the quotient of a Banach space by a subspace is complete.

theorem isUniformEmbedding_translate_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (a : α) : IsUniformEmbedding fun (x : α) => x * a

theorem isUniformEmbedding_translate_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) : IsUniformEmbedding fun (x : α) => x + a

theorem IsUniformGroup.cauchy_iff_tendsto {G : Type u_4} [Group G] [UniformSpace G] [IsUniformGroup G] (𝓕 : Filter G) : Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : G × G) => p.1 / p.2) (𝓕 ×ˢ 𝓕) (nhds 1)

theorem IsUniformAddGroup.cauchy_iff_tendsto {G : Type u_4} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] (𝓕 : Filter G) : Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : G × G) => p.1 - p.2) (𝓕 ×ˢ 𝓕) (nhds 0)

theorem IsUniformGroup.cauchy_iff_tendsto_swapped {G : Type u_4} [Group G] [UniformSpace G] [IsUniformGroup G] (𝓕 : Filter G) : Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : G × G) => p.2 / p.1) (𝓕 ×ˢ 𝓕) (nhds 1)

theorem IsUniformAddGroup.cauchy_iff_tendsto_swapped {G : Type u_4} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] (𝓕 : Filter G) : Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : G × G) => p.2 - p.1) (𝓕 ×ˢ 𝓕) (nhds 0)

theorem IsUniformGroup.cauchy_map_iff_tendsto {ι : Type u_3} {G : Type u_4} [Group G] [UniformSpace G] [IsUniformGroup G] (𝓕 : Filter ι) (f : ι → G) : Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : ι × ι) => f p.1 / f p.2) (𝓕 ×ˢ 𝓕) (nhds 1)

theorem IsUniformAddGroup.cauchy_map_iff_tendsto {ι : Type u_3} {G : Type u_4} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] (𝓕 : Filter ι) (f : ι → G) : Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : ι × ι) => f p.1 - f p.2) (𝓕 ×ˢ 𝓕) (nhds 0)

theorem IsUniformGroup.cauchy_map_iff_tendsto_swapped {ι : Type u_3} {G : Type u_4} [Group G] [UniformSpace G] [IsUniformGroup G] (𝓕 : Filter ι) (f : ι → G) : Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : ι × ι) => f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (nhds 1)

theorem IsUniformAddGroup.cauchy_map_iff_tendsto_swapped {ι : Type u_3} {G : Type u_4} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] (𝓕 : Filter ι) (f : ι → G) : Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : ι × ι) => f p.2 - f p.1) (𝓕 ×ˢ 𝓕) (nhds 0)

theorem IsRightUniformGroup.completeSpace_of_weaklyLocallyCompactSpace {G : Type u_3} [Group G] [UniformSpace G] [IsRightUniformGroup G] [WeaklyLocallyCompactSpace G] : CompleteSpace G

A locally compact right-uniform group is complete.

theorem IsRightUniformAddGroup.completeSpace_of_weaklyLocallyCompactSpace {G : Type u_3} [AddGroup G] [UniformSpace G] [IsRightUniformAddGroup G] [WeaklyLocallyCompactSpace G] : CompleteSpace G

A locally compact right-uniform additive group is complete.

instance Subgroup.isUniformGroup {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] (S : Subgroup α) : IsUniformGroup ↥S

instance AddSubgroup.isUniformAddGroup {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (S : AddSubgroup α) : IsUniformAddGroup ↥S

theorem CauchySeq.mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} [Preorder ι] {u v : ι → α} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (u * v)

theorem CauchySeq.add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} [Preorder ι] {u v : ι → α} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (u + v)

theorem CauchySeq.mul_const {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun (n : ι) => u n * x

theorem CauchySeq.add_const {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun (n : ι) => u n + x

theorem CauchySeq.const_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun (n : ι) => x * u n

theorem CauchySeq.const_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun (n : ι) => x + u n

theorem CauchySeq.inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} (h : CauchySeq u) : CauchySeq u⁻¹

theorem CauchySeq.neg {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} [Preorder ι] {u : ι → α} (h : CauchySeq u) : CauchySeq (-u)

theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {s : Set α} : TotallyBounded s ↔ ∀ U ∈ nhds 1, ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U

theorem totallyBounded_iff_subset_finite_iUnion_nhds_zero {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {s : Set α} : TotallyBounded s ↔ ∀ U ∈ nhds 0, ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U

theorem totallyBounded_inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {s : Set α} (hs : TotallyBounded s) : TotallyBounded s⁻¹

theorem totallyBounded_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {s : Set α} (hs : TotallyBounded s) : TotallyBounded (-s)

theorem TendstoUniformlyOnFilter.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f * f') (g * g') l l'

theorem TendstoUniformlyOnFilter.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f + f') (g + g') l l'

theorem TendstoUniformlyOnFilter.fun_add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (fun (i : ι) (i_1 : β) => f i i_1 + f' i i_1) (fun (i : β) => g i + g' i) l l'

Eta-expanded form of TendstoUniformlyOnFilter.add

theorem TendstoUniformlyOnFilter.fun_mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (fun (i : ι) (i_1 : β) => f i i_1 * f' i i_1) (fun (i : β) => g i * g' i) l l'

Eta-expanded form of TendstoUniformlyOnFilter.mul

theorem TendstoUniformlyOnFilter.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f / f') (g / g') l l'

theorem TendstoUniformlyOnFilter.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f - f') (g - g') l l'

theorem TendstoUniformlyOnFilter.fun_div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (fun (i : ι) (i_1 : β) => f i i_1 / f' i i_1) (fun (i : β) => g i / g' i) l l'

Eta-expanded form of TendstoUniformlyOnFilter.div

theorem TendstoUniformlyOnFilter.fun_sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (fun (i : ι) (i_1 : β) => f i i_1 - f' i i_1) (fun (i : β) => g i - g' i) l l'

Eta-expanded form of TendstoUniformlyOnFilter.sub

theorem TendstoUniformlyOnFilter.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ι → β → α} {g : β → α} (hf : TendstoUniformlyOnFilter f g l l') : TendstoUniformlyOnFilter f⁻¹ g⁻¹ l l'

theorem TendstoUniformlyOnFilter.neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ι → β → α} {g : β → α} (hf : TendstoUniformlyOnFilter f g l l') : TendstoUniformlyOnFilter (-f) (-g) l l'

theorem TendstoUniformlyOnFilter.fun_inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ι → β → α} {g : β → α} (hf : TendstoUniformlyOnFilter f g l l') : TendstoUniformlyOnFilter (fun (i : ι) (i_1 : β) => (f i i_1)⁻¹) (fun (i : β) => (g i)⁻¹) l l'

Eta-expanded form of TendstoUniformlyOnFilter.inv

theorem TendstoUniformlyOnFilter.fun_neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {l' : Filter β} {f : ι → β → α} {g : β → α} (hf : TendstoUniformlyOnFilter f g l l') : TendstoUniformlyOnFilter (fun (i : ι) (i_1 : β) => -f i i_1) (fun (i : β) => -g i) l l'

Eta-expanded form of TendstoUniformlyOnFilter.neg

theorem TendstoUniformlyOn.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f * f') (g * g') l s

theorem TendstoUniformlyOn.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f + f') (g + g') l s

theorem TendstoUniformlyOn.fun_add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (fun (i : ι) (i_1 : β) => f i i_1 + f' i i_1) (fun (i : β) => g i + g' i) l s

Eta-expanded form of TendstoUniformlyOn.add

theorem TendstoUniformlyOn.fun_mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (fun (i : ι) (i_1 : β) => f i i_1 * f' i i_1) (fun (i : β) => g i * g' i) l s

Eta-expanded form of TendstoUniformlyOn.mul

theorem TendstoUniformlyOn.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f / f') (g / g') l s

theorem TendstoUniformlyOn.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f - f') (g - g') l s

theorem TendstoUniformlyOn.fun_div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (fun (i : ι) (i_1 : β) => f i i_1 / f' i i_1) (fun (i : β) => g i / g' i) l s

Eta-expanded form of TendstoUniformlyOn.div

theorem TendstoUniformlyOn.fun_sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (fun (i : ι) (i_1 : β) => f i i_1 - f' i i_1) (fun (i : β) => g i - g' i) l s

Eta-expanded form of TendstoUniformlyOn.sub

theorem TendstoUniformlyOn.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {g : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) : TendstoUniformlyOn f⁻¹ g⁻¹ l s

theorem TendstoUniformlyOn.neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {g : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) : TendstoUniformlyOn (-f) (-g) l s

theorem TendstoUniformlyOn.fun_inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {g : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) : TendstoUniformlyOn (fun (i : ι) (i_1 : β) => (f i i_1)⁻¹) (fun (i : β) => (g i)⁻¹) l s

Eta-expanded form of TendstoUniformlyOn.inv

theorem TendstoUniformlyOn.fun_neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {g : β → α} {s : Set β} (hf : TendstoUniformlyOn f g l s) : TendstoUniformlyOn (fun (i : ι) (i_1 : β) => -f i i_1) (fun (i : β) => -g i) l s

Eta-expanded form of TendstoUniformlyOn.neg

theorem TendstoUniformly.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f * f') (g * g') l

theorem TendstoUniformly.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f + f') (g + g') l

theorem TendstoUniformly.fun_mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (fun (i : ι) (i_1 : β) => f i i_1 * f' i i_1) (fun (i : β) => g i * g' i) l

Eta-expanded form of TendstoUniformly.mul

theorem TendstoUniformly.fun_add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (fun (i : ι) (i_1 : β) => f i i_1 + f' i i_1) (fun (i : β) => g i + g' i) l

Eta-expanded form of TendstoUniformly.add

theorem TendstoUniformly.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f / f') (g / g') l

theorem TendstoUniformly.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f - f') (g - g') l

theorem TendstoUniformly.fun_div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (fun (i : ι) (i_1 : β) => f i i_1 / f' i i_1) (fun (i : β) => g i / g' i) l

Eta-expanded form of TendstoUniformly.div

theorem TendstoUniformly.fun_sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (fun (i : ι) (i_1 : β) => f i i_1 - f' i i_1) (fun (i : β) => g i - g' i) l

Eta-expanded form of TendstoUniformly.sub

theorem TendstoUniformly.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {g : β → α} (hf : TendstoUniformly f g l) : TendstoUniformly f⁻¹ g⁻¹ l

theorem TendstoUniformly.neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {g : β → α} (hf : TendstoUniformly f g l) : TendstoUniformly (-f) (-g) l

theorem TendstoUniformly.fun_inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {g : β → α} (hf : TendstoUniformly f g l) : TendstoUniformly (fun (i : ι) (i_1 : β) => (f i i_1)⁻¹) (fun (i : β) => (g i)⁻¹) l

Eta-expanded form of TendstoUniformly.inv

theorem TendstoUniformly.fun_neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {g : β → α} (hf : TendstoUniformly f g l) : TendstoUniformly (fun (i : ι) (i_1 : β) => -f i i_1) (fun (i : β) => -g i) l

Eta-expanded form of TendstoUniformly.neg

theorem UniformCauchySeqOn.mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f * f') l s

theorem UniformCauchySeqOn.add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f + f') l s

theorem UniformCauchySeqOn.fun_mul {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (fun (i : ι) (i_1 : β) => f i i_1 * f' i i_1) l s

Eta-expanded form of UniformCauchySeqOn.mul

theorem UniformCauchySeqOn.fun_add {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (fun (i : ι) (i_1 : β) => f i i_1 + f' i i_1) l s

Eta-expanded form of UniformCauchySeqOn.add

theorem UniformCauchySeqOn.div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f / f') l s

theorem UniformCauchySeqOn.sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f - f') l s

theorem UniformCauchySeqOn.fun_sub {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (fun (i : ι) (i_1 : β) => f i i_1 - f' i i_1) l s

Eta-expanded form of UniformCauchySeqOn.sub

theorem UniformCauchySeqOn.fun_div {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f f' : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (fun (i : ι) (i_1 : β) => f i i_1 / f' i i_1) l s

Eta-expanded form of UniformCauchySeqOn.div

theorem UniformCauchySeqOn.inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) : UniformCauchySeqOn f⁻¹ l s

theorem UniformCauchySeqOn.neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) : UniformCauchySeqOn (-f) l s

theorem UniformCauchySeqOn.fun_neg {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) : UniformCauchySeqOn (fun (i : ι) (i_1 : β) => -f i i_1) l s

Eta-expanded form of UniformCauchySeqOn.neg

theorem UniformCauchySeqOn.fun_inv {α : Type u_1} {β : Type u_2} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {l : Filter ι} {f : ι → β → α} {s : Set β} (hf : UniformCauchySeqOn f l s) : UniformCauchySeqOn (fun (i : ι) (i_1 : β) => (f i i_1)⁻¹) l s

Eta-expanded form of UniformCauchySeqOn.inv

theorem TendstoLocallyUniformlyOn.mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) (hg : TendstoLocallyUniformlyOn G g l s) : TendstoLocallyUniformlyOn (F * G) (f * g) l s

theorem TendstoLocallyUniformlyOn.add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) (hg : TendstoLocallyUniformlyOn G g l s) : TendstoLocallyUniformlyOn (F + G) (f + g) l s

theorem TendstoLocallyUniformlyOn.fun_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) (hg : TendstoLocallyUniformlyOn G g l s) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => F i i_1 * G i i_1) (fun (i : X) => f i * g i) l s

Eta-expanded form of TendstoLocallyUniformlyOn.mul

theorem TendstoLocallyUniformlyOn.fun_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) (hg : TendstoLocallyUniformlyOn G g l s) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => F i i_1 + G i i_1) (fun (i : X) => f i + g i) l s

Eta-expanded form of TendstoLocallyUniformlyOn.add

theorem TendstoLocallyUniformlyOn.div {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) (hg : TendstoLocallyUniformlyOn G g l s) : TendstoLocallyUniformlyOn (F / G) (f / g) l s

theorem TendstoLocallyUniformlyOn.sub {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) (hg : TendstoLocallyUniformlyOn G g l s) : TendstoLocallyUniformlyOn (F - G) (f - g) l s

theorem TendstoLocallyUniformlyOn.fun_div {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) (hg : TendstoLocallyUniformlyOn G g l s) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => F i i_1 / G i i_1) (fun (i : X) => f i / g i) l s

Eta-expanded form of TendstoLocallyUniformlyOn.div

theorem TendstoLocallyUniformlyOn.fun_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) (hg : TendstoLocallyUniformlyOn G g l s) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => F i i_1 - G i i_1) (fun (i : X) => f i - g i) l s

Eta-expanded form of TendstoLocallyUniformlyOn.sub

theorem TendstoLocallyUniformlyOn.inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) : TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s

theorem TendstoLocallyUniformlyOn.neg {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) : TendstoLocallyUniformlyOn (-F) (-f) l s

theorem TendstoLocallyUniformlyOn.fun_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => -F i i_1) (fun (i : X) => -f i) l s

Eta-expanded form of TendstoLocallyUniformlyOn.neg

theorem TendstoLocallyUniformlyOn.fun_inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {s : Set X} {l : Filter ι} (hf : TendstoLocallyUniformlyOn F f l s) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l s

Eta-expanded form of TendstoLocallyUniformlyOn.inv

theorem TendstoLocallyUniformly.mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) (hg : TendstoLocallyUniformly G g l) : TendstoLocallyUniformly (F * G) (f * g) l

theorem TendstoLocallyUniformly.add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) (hg : TendstoLocallyUniformly G g l) : TendstoLocallyUniformly (F + G) (f + g) l

theorem TendstoLocallyUniformly.fun_mul {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) (hg : TendstoLocallyUniformly G g l) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => F i i_1 * G i i_1) (fun (i : X) => f i * g i) l

Eta-expanded form of TendstoLocallyUniformly.mul

theorem TendstoLocallyUniformly.fun_add {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) (hg : TendstoLocallyUniformly G g l) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => F i i_1 + G i i_1) (fun (i : X) => f i + g i) l

Eta-expanded form of TendstoLocallyUniformly.add

theorem TendstoLocallyUniformly.div {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) (hg : TendstoLocallyUniformly G g l) : TendstoLocallyUniformly (F / G) (f / g) l

theorem TendstoLocallyUniformly.sub {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) (hg : TendstoLocallyUniformly G g l) : TendstoLocallyUniformly (F - G) (f - g) l

theorem TendstoLocallyUniformly.fun_div {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) (hg : TendstoLocallyUniformly G g l) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => F i i_1 / G i i_1) (fun (i : X) => f i / g i) l

Eta-expanded form of TendstoLocallyUniformly.div

theorem TendstoLocallyUniformly.fun_sub {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) (hg : TendstoLocallyUniformly G g l) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => F i i_1 - G i i_1) (fun (i : X) => f i - g i) l

Eta-expanded form of TendstoLocallyUniformly.sub

theorem TendstoLocallyUniformly.inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) : TendstoLocallyUniformly F⁻¹ f⁻¹ l

theorem TendstoLocallyUniformly.neg {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) : TendstoLocallyUniformly (-F) (-f) l

theorem TendstoLocallyUniformly.fun_inv {α : Type u_1} [UniformSpace α] [Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l

Eta-expanded form of TendstoLocallyUniformly.inv

theorem TendstoLocallyUniformly.fun_neg {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι} (hf : TendstoLocallyUniformly F f l) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => -F i i_1) (fun (i : X) => -f i) l

Eta-expanded form of TendstoLocallyUniformly.neg

@[instance 100]

instance IsUniformGroup.of_compactSpace {β : Type u_2} [UniformSpace β] [Group β] [ContinuousDiv β] [CompactSpace β] : IsUniformGroup β

@[instance 100]

instance IsUniformAddGroup.of_compactSpace {β : Type u_2} [UniformSpace β] [AddGroup β] [ContinuousSub β] [CompactSpace β] : IsUniformAddGroup β

@[deprecated IsUniformGroup.of_compactSpace (since := "2025-09-27")]

theorem topologicalGroup_is_uniform_of_compactSpace (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : IsUniformGroup G

@[deprecated IsUniformGroup.of_compactSpace (since := "2025-09-27")]

theorem topologicalAddGroup_is_uniform_of_compactSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] : IsUniformAddGroup G

instance Subgroup.isClosed_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H : Subgroup G} [DiscreteTopology ↥H] : IsClosed ↑H

instance AddSubgroup.isClosed_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {H : AddSubgroup G} [DiscreteTopology ↥H] : IsClosed ↑H

theorem Subgroup.tendsto_coe_cofinite_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (H : Subgroup G) (hH : IsDiscrete ↑H) : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)

theorem AddSubgroup.tendsto_coe_cofinite_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] (H : AddSubgroup G) (hH : IsDiscrete ↑H) : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)

theorem MonoidHom.tendsto_coe_cofinite_of_discrete {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H : Type u_2} [Group H] {f : H →* G} (hf : Function.Injective ⇑f) (hf' : IsDiscrete ↑f.range) : Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)

theorem AddMonoidHom.tendsto_coe_cofinite_of_discrete {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {H : Type u_2} [AddGroup H] {f : H →+ G} (hf : Function.Injective ⇑f) (hf' : IsDiscrete ↑f.range) : Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)

theorem MulOpposite.comap_op_rightUniformSpace (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : UniformSpace.comap op (IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.leftUniformSpace G

theorem AddOpposite.comap_op_rightUniformSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace.comap op (IsTopologicalAddGroup.rightUniformSpace Gᵃᵒᵖ) = IsTopologicalAddGroup.leftUniformSpace G

theorem MulOpposite.comap_op_leftUniformSpace (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : UniformSpace.comap op (IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.rightUniformSpace G

theorem AddOpposite.comap_op_leftUniformSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace.comap op (IsTopologicalAddGroup.leftUniformSpace Gᵃᵒᵖ) = IsTopologicalAddGroup.rightUniformSpace G

def MulOpposite.opUniformEquivRight (G : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : G ≃ᵤ Gᵐᵒᵖ

The equivalence between a topological group G and Gᵐᵒᵖ as a uniform equivalence when G is equipped with the right uniformity and Gᵐᵒᵖ with the left uniformity.

def AddOpposite.opUniformEquivRight (G : Type u_2) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : G ≃ᵤ Gᵃᵒᵖ

The equivalence between an additive topological group G and Gᵐᵒᵖ as a uniform equivalence when G is equipped with the right uniformity and Gᵐᵒᵖ with the left uniformity.

def MulOpposite.opUniformEquivLeft (G : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : G ≃ᵤ Gᵐᵒᵖ

The equivalence between a topological group G and Gᵐᵒᵖ as a uniform equivalence when G is equipped with the left uniformity and Gᵐᵒᵖ with the right uniformity.

def AddOpposite.opUniformEquivLeft (G : Type u_2) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : G ≃ᵤ Gᵃᵒᵖ

The equivalence between an additive topological group G and Gᵃᵒᵖ as a uniform equivalence when G is equipped with the left uniformity and Gᵃᵒᵖ with the right uniformity.

theorem comap_inv_leftUniformSpace (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : UniformSpace.comap (⇑(Equiv.inv G)) (IsTopologicalGroup.leftUniformSpace G) = IsTopologicalGroup.rightUniformSpace G

theorem comap_neg_leftUniformSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace.comap (⇑(Equiv.neg G)) (IsTopologicalAddGroup.leftUniformSpace G) = IsTopologicalAddGroup.rightUniformSpace G

def UniformEquiv.inv (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : G ≃ᵤ G

Inversion on a topological group, as a uniform equivalence between the right uniformity and the left uniformity.

def UniformEquiv.neg (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : G ≃ᵤ G

Negation on an additive topological group, as a uniform equivalence between the right uniformity and the left uniformity.

theorem IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CompleteSpace G ↔ CompleteSpace G

theorem IsTopologicalAddGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : CompleteSpace G ↔ CompleteSpace G

theorem IsTopologicalGroup.tendstoUniformly_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [IsTopologicalGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : rightUniformSpace G = u) : TendstoUniformly F f p ↔ ∀ u_1 ∈ nhds 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u_1

theorem IsTopologicalAddGroup.tendstoUniformly_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : rightUniformSpace G = u) : TendstoUniformly F f p ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a ∈ u_1

theorem IsTopologicalGroup.tendstoUniformlyOn_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [IsTopologicalGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : rightUniformSpace G = u) : TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 1, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a / f a ∈ u_1

theorem IsTopologicalAddGroup.tendstoUniformlyOn_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : rightUniformSpace G = u) : TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a - f a ∈ u_1

theorem IsTopologicalGroup.tendstoLocallyUniformly_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [IsTopologicalGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : rightUniformSpace G = u) : TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ nhds 1, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1

theorem IsTopologicalAddGroup.tendstoLocallyUniformly_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : rightUniformSpace G = u) : TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ nhds 0, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1

theorem IsTopologicalGroup.tendstoLocallyUniformlyOn_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [IsTopologicalGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : rightUniformSpace G = u) : TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 1, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1

theorem IsTopologicalAddGroup.tendstoLocallyUniformlyOn_iff {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : rightUniformSpace G = u) : TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1

theorem tendsto_div_comap_self {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [Group α] [IsTopologicalGroup α] [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 α] [IsTopologicalAddGroup α] [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)

theorem IsDenseInducing.extend_Z_bilin {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [TopologicalSpace α] [AddCommGroup α] [IsTopologicalAddGroup α] [TopologicalSpace β] [AddCommGroup β] [TopologicalSpace γ] [AddCommGroup γ] [IsTopologicalAddGroup γ] [TopologicalSpace δ] [AddCommGroup δ] [UniformSpace G] [AddCommGroup G] {e : β →+ α} (de : IsDenseInducing ⇑e) {f : δ →+ γ} (df : IsDenseInducing ⇑f) {φ : β →+ δ →+ G} (hφ : Continuous fun (p : β × δ) => (φ p.1) p.2) [IsUniformAddGroup G] [T0Space G] [CompleteSpace G] : Continuous (⋯.extend fun (p : β × δ) => (φ p.1) p.2)

Bourbaki GT III.6.5 Theorem I: ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity. Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary.

instance QuotientGroup.completeSpace_right' (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal] [CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable topological group G by a normal subgroup is itself complete. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Because a topological group is not equipped with a UniformSpace instance by default, we must explicitly provide it in order to consider completeness. See QuotientGroup.completeSpace_right for a version in which G is already equipped with a uniform structure.

instance QuotientAddGroup.completeSpace_right' (G : Type u) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable topological additive group G by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by subspaces are complete. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Because an additive topological group is not equipped with a UniformSpace instance by default, we must explicitly provide it in order to consider completeness. See QuotientAddGroup.completeSpace_right for a version in which G is already equipped with a uniform structure.

instance QuotientGroup.completeSpace_right (G : Type u_1) [Group G] [us : UniformSpace G] [IsRightUniformGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable uniform group G by a normal subgroup is itself complete. In contrast to QuotientGroup.completeSpace_right', in this version G is already equipped with a uniform structure. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Even though G is equipped with a uniform structure, the quotient G ⧸ N does not inherit a uniform structure, so it is still provided manually via IsTopologicalGroup.rightUniformSpace. In the most common use cases, this coincides (definitionally) with the uniform structure on the quotient obtained via other means.

instance QuotientAddGroup.completeSpace_right (G : Type u_1) [AddGroup G] [us : UniformSpace G] [IsRightUniformAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable uniform additive group G by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by subspaces are complete. In contrast to QuotientAddGroup.completeSpace_right', in this version G is already equipped with a uniform structure. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Even though G is equipped with a uniform structure, the quotient G ⧸ N does not inherit a uniform structure, so it is still provided manually via IsTopologicalAddGroup.rightUniformSpace. In the most common use case ─ quotients of normed additive commutative groups by subgroups ─ significant care was taken so that the uniform structure inherent in that setting coincides (definitionally) with the uniform structure provided here.

instance QuotientGroup.completeSpace_left' (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable topological group G by a normal subgroup is itself complete. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Because a topological group is not equipped with a UniformSpace instance by default, we must explicitly provide it in order to consider completeness. See QuotientGroup.completeSpace_left for a version in which G is already equipped with a uniform structure.

instance QuotientAddGroup.completeSpace_left' (G : Type u) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable topological additive group G by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by subspaces are complete. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Because an additive topological group is not equipped with a UniformSpace instance by default, we must explicitly provide it in order to consider completeness. See QuotientAddGroup.completeSpace_left for a version in which G is already equipped with a uniform structure.

instance QuotientGroup.completeSpace_left (G : Type u_1) [Group G] [us : UniformSpace G] [IsLeftUniformGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable uniform group G by a normal subgroup is itself complete. In contrast to QuotientGroup.completeSpace_left', in this version G is already equipped with a uniform structure. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Even though G is equipped with a uniform structure, the quotient G ⧸ N does not inherit a uniform structure, so it is still provided manually via IsTopologicalGroup.leftUniformSpace. In the most common use cases, this coincides (definitionally) with the uniform structure on the quotient obtained via other means.

instance QuotientAddGroup.completeSpace_left (G : Type u_1) [AddGroup G] [us : UniformSpace G] [IsLeftUniformAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)

The quotient G ⧸ N of a complete first countable uniform additive group G by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by subspaces are complete. In contrast to QuotientAddGroup.completeSpace_left', in this version G is already equipped with a uniform structure. [N. Bourbaki, General Topology, IX.3.1 Proposition 4][bourbaki1966b]

Even though G is equipped with a uniform structure, the quotient G ⧸ N does not inherit a uniform structure, so it is still provided manually via IsTopologicalAddGroup.leftUniformSpace.