cauchy_map_iff' — Mathlib

English

A variant stating the equivalence for l.map f with a primed form identical to cauchy_map_iff.

Русский

Вариант, формулирующий эквивалентность для l.map f в аналогичном виде к cauchy_map_iff.

LaTeX

$$$ {l:\text{Filter }\beta} \;{f:\beta\to\alpha}:\; \text{Cauchy}(\text{Filter.map } f\ l) \iff \text{NeBot}(l) \land \text{Tendsto}(\lambda p:β×β, (f\ p.1, f\ p.2))\ (l×ˢ l) (𝓤\_α)$$$

Lean4

theorem cauchy_map_iff' {l : Filter β} [hl : NeBot l] {f : β → α} :
    Cauchy (l.map f) ↔ Tendsto (fun p : β × β => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α) :=
  cauchy_map_iff.trans <| and_iff_right hl

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