cauchy_prod_iff — Mathlib

English

For F a filter on α×β, Cauchy F is equivalent to Cauchy of its projections on α and β.

Русский

Для фильтра F на α×β условие Коши эквивалентно Коши проекций на α и β.

LaTeX

$$$ \text{Cauchy}(F) \iff \text{Cauchy}(\text{map Prod.fst } F) \land \text{Cauchy}(\text{map Prod.snd } F)$$$

Lean4

theorem cauchy_prod_iff [UniformSpace β] {F : Filter (α × β)} :
    Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F) := by
  simp_rw [instUniformSpaceProd, ← cauchy_comap_uniformSpace, ← cauchy_inf_uniformSpace]

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