Theorems · Theorem · Lie groups

IsTopologicalGroup.tendstoLocallyUniformly_iff

∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Group G] [u : UniformSpace G] [inst_1 : IsTopologicalGroup G]
  [inst_2 : TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι),
  IsTopologicalGroup.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)

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Basic

Cited by

0 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupUniformSpaceIsTopologicalGroupTopologicalSpace