cauchy_map_iff_tendsto — Mathlib

English

For a map f from ι to G, the image filter map f 𝓕 is Cauchy iff 𝓕 is nontrivial and Tendsto of (f p.1)/(f p.2) to the identity holds.

Русский

Для отображения f: ι → G, образующий фильтр map f 𝓕, является Cauchy тогда и только тогда, когда 𝓕 непуст и выполняется предел Tendsto для (f p.1)/(f p.2) к единице.

LaTeX

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

Lean4

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

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