cauchy_iff_tendsto — Mathlib

English

For a group G with a uniform structure, a filter 𝓕 is Cauchy iff it is nontrivial and the pairwise quotients converge to the identity 1.

Русский

Для группы G с равномерной структурой фильтр 𝓕 является Cauchy тогда и только тогда, когда он не тривиален и пары элементов сходятся к единице 1 через отношение деления.

LaTeX

$$$\\mathrm{Cauchy}(\\mathscr{F}) \\iff \\mathscr{F} \\neq 0 \\land \\mathrm{Tendsto}(p \\mapsto p_1/p_2) (\\mathscr{F} \\times\\mathscr{F}) (\\mathcal{N}(1))$$$

Lean4

@[to_additive]
theorem cauchy_iff_tendsto (𝓕 : Filter G) : Cauchy 𝓕 ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ p.1 / p.2) (𝓕 ×ˢ 𝓕) (𝓝 1) := by
  simp [Cauchy, uniformity_eq_comap_nhds_one_swapped, ← tendsto_iff_comap]

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