UniformCauchySeqOn — Mathlib

English

A sequence is uniformly Cauchy on a set if pairwise differences are uniformly bounded for all x in the set and indices in p.

Русский

Последовательность равномерно коши на множестве, если пары значений различий по x в множестве ограничены единообразно по индексам.

LaTeX

$$$UniformCauchySeqOn F p s :="\\forall u\\in 𝓤(β),\\forallᶠ m : (ι\\times ι)\\times α \\ in (p\\timesˢ p)\\timesˢ p',\\ (F m.fst.fst m.snd, F m.fst.snd m.snd) \\in u$$$

Lean4

/-- A sequence is uniformly Cauchy if eventually all of its pairwise differences are
uniformly bounded -/
def UniformCauchySeqOn (F : ι → α → β) (p : Filter ι) (s : Set α) : Prop :=
  ∀ u ∈ 𝓤 β, ∀ᶠ m : ι × ι in p ×ˢ p, ∀ x : α, x ∈ s → (F m.fst x, F m.snd x) ∈ u

Похожие утверждения