Theorems · Theorem · functional analysis

SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one

∀ {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [inst : SeminormedGroup G] {f : ι → κ → G} {l : Filter ι}
  {l' : Filter κ},
  UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z => (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'

Defined in

Mathlib.Analysis.Normed.Group.Continuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedGroup