cauchy_map — Mathlib

English

For a fixed x ∈ s, the sequence i ↦ F i x is Cauchy in β with respect to p.

Русский

Для фиксированного x ∈ s последовательность i ↦ F i x является Коши в β по отношению к p.

LaTeX

$$$$ \\forall x \\in s,\\; Cauchy(\\mathrm{map}(i \\mapsto F i x, p)). $$$$

Lean4

/-- If a sequence of functions is uniformly Cauchy on a set, then the values at each point form
a Cauchy sequence. -/
theorem cauchy_map [hp : NeBot p] (hf : UniformCauchySeqOn F p s) (hx : x ∈ s) : Cauchy (map (fun i => F i x) p) :=
  by
  simp only [cauchy_map_iff, hp, true_and]
  intro u hu
  rw [mem_map]
  filter_upwards [hf u hu] with p hp using hp x hx

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