cauchy_map_iff_tendsto_swapped — Mathlib

English

For a map f: ι → G, Cauchy for map f 𝓕 is equivalent to nontrivial 𝓕 and Tendsto for the swapped quotient.

Русский

Для отображения f: ι → G, Cauchy для map f 𝓕 эквивалентно не тривиальному 𝓕 и предел Tendsto для обратного отношения.

LaTeX

$$$\\mathrm{Cauchy}(\\mathrm{map}\\ f\\ 𝓕) \\iff 𝓕 \\neq 0 \\land \\mathrm{Tendsto}\\big(\\lambda p. (f\\,p.2) / (f\\,p.1)\\big) (𝓕 \\times 𝓕) (\\mathcal{N}(1))$$$

Lean4

@[to_additive]
theorem cauchy_map_iff_tendsto_swapped (𝓕 : Filter ι) (f : ι → G) :
    Cauchy (map f 𝓕) ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (𝓝 1) := by
  simp [cauchy_map_iff, uniformity_eq_comap_nhds_one, Function.comp_def]

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