cauchy_pi_iff' — Mathlib

English

For a filter l on Π i α_i with l ≠ ⊥, we have Cauchy l iff ∀ i, Cauchy (map (eval i) l).

Русский

Для фильтра l на произведении Π i α_i, если l ≠ ⊥, тогда Cauchy l эквивалентно ∀ i, Cauchy (map (eval i) l).

LaTeX

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

Lean4

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

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