of_curry — Mathlib

English

If ∃ᶠ x in la, ∃ᶠ y in lb, p (x,y), then ∃ᶠ xy in la × lb, p xy.

Русский

Если есть частотная пара x,y с p(x,y), то ∃ᶠ (x,y) в ла×lb: p(x,y).

LaTeX

$$$$\exists^\infty x \in la, \exists^\infty y \in lb, p(x,y) \Rightarrow \exists^\infty (x,y) \in la \times lb, p(x,y).$$$$

Lean4

theorem of_curry {la : Filter α} {lb : Filter β} {p : α × β → Prop} (h : ∃ᶠ x in la, ∃ᶠ y in lb, p (x, y)) :
    ∃ᶠ xy in la ×ˢ lb, p xy :=
  h.uncurry

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