Theorems · Theorem · Lie groups

IsUniformGroup.cauchy_map_iff_tendsto

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

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupUniformSpaceIsUniformGroup