cauchy_pi_iff — Mathlib

English

Let ι be nonempty. For a filter l on ∏ i α_i, l is Cauchy if and only if for every i, the projection map to α_i sends l to a Cauchy filter on α_i.

Русский

Пусть ι непусто. Тогда фильтр l на ∏ i α_i равномерно полный (Cauchy) тогда и только тогда, когда для каждого i проецирующий отображение на α_i отправляет l в Cauchy-фильтр на α_i.

LaTeX

$$$\\text{Cauchy } l \\iff \\forall i, \\text{Cauchy} (map (eval i) l)$$$

Lean4

theorem cauchy_pi_iff [Nonempty ι] {l : Filter (∀ i, α i)} : Cauchy l ↔ ∀ i, Cauchy (map (eval i) l) := by
  simp_rw [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace, cauchy_comap_uniformSpace]

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