prod — Mathlib

English

If α and β are uniform spaces, then F is Cauchy on α×β iff the projections are Cauchy.

Русский

Если пространства α и β равномерны, то фильтр F на α×β является Коши тогда и только тогда, когда проекции на α и β являются Коши.

LaTeX

$$$ \forall {α β},\ [\text{UniformSpace } α] [\text{UniformSpace } β] \; {F : Filter (α × β)}:\; \text{Cauchy}(F) \iff \text{Cauchy}(\text{map Prod.fst } F) ∧ \text{Cauchy}(\text{map Prod.snd } F)$$$

Lean4

theorem prod [UniformSpace β] {f : Filter α} {g : Filter β} (hf : Cauchy f) (hg : Cauchy g) : Cauchy (f ×ˢ g) :=
  by
  have := hf.1; have := hg.1
  simpa [cauchy_prod_iff, hf.1] using ⟨hf, hg⟩

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