tendsto_uniformity — Mathlib

English

If u: γ → α and v: δ → β are Cauchy sequences, then the paired sequence Prod.map u v: γ → α × β is Cauchy.

Русский

Если u: γ → α и v: δ → β — обе Коши-последовательности, тогда последовательность, заданная как (u,g) × (v,h) через prodMap, является Коши.

LaTeX

$$$(u:\\gamma\\to\\alpha)$, $(v:\\delta\\to\\beta)$;\\quad CauchySeq(u) \\land CauchySeq(v) \\Rightarrow CauchySeq(\\mathrm{ProdMap}(u,v)).$$$

Lean4

theorem tendsto_uniformity [Preorder β] {u : β → α} (h : CauchySeq u) : Tendsto (Prod.map u u) atTop (𝓤 α) := by
  simpa only [Tendsto, prod_map_map_eq', prod_atTop_atTop_eq] using h.right

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