cauchy_map_iff_exists_tendsto — Mathlib

English

If l is a filter on β and f: β → α with α complete, then Cauchy (l.map f) iff ∃ x, Tendsto f l (nhds x).

Русский

Если l — фильтр на β и f: β → α, то при полной пространстве α, из Cauchy (l.map f) следует ∃ x, Tendsto f l (nhds x).

LaTeX

$$$Cauchy(l.map f) \\iff \\exists x, Tendsto f\\, l\\, (nhds\\ x)$$$

Lean4

theorem cauchy_map_iff_exists_tendsto [CompleteSpace α] {l : Filter β} {f : β → α} [NeBot l] :
    Cauchy (l.map f) ↔ ∃ x, Tendsto f l (𝓝 x) :=
  cauchy_iff_exists_le_nhds

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