cauchy_map — Mathlib

English

If f: β → α tends to nhds a along l, then map f l is Cauchy.

Русский

Если отображение f: β → α стремится к некоторой окрестности a вдоль l, то образованный фильтр map f l является Коши.

LaTeX

$$$ \text{Tendsto } f\ l\ (\text{nhds } a) \Rightarrow \text{Cauchy}(\text{map } f\ l)$$$

Lean4

theorem cauchy_map {l : Filter β} [NeBot l] {f : β → α} {a : α} (h : Tendsto f l (𝓝 a)) : Cauchy (map f l) :=
  cauchy_nhds.mono h

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