cauchy_map_iff — Mathlib

English

Let l be a filter on β, f: β → α a map, then Cauchy (l.map f) holds iff NeBot(l) and Tendsto (f p.1, f p.2) along l × l tends to the uniformity on α.

Русский

Пусть l — фильтр на β, f: β → α — отображение. Тогда Cauchy (l.map f) эквивалентно NeBot(l) и стремление пары (f p1, f p2) по l × l к равномерности α.

LaTeX

$$$ \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 β} {f : β → α} :
    Cauchy (l.map f) ↔ NeBot l ∧ Tendsto (fun p : β × β => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α) := by
  rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]

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