uncurry — Mathlib

English

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

Русский

Если существуют часто встречающиеся значения x в ла и y в lb, такие что 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 xy \in la \times lb, p(xy).$$$$

Lean4

protected theorem uncurry {la : Filter α} {lb : Filter β} {p : α → β → Prop} (h : ∃ᶠ x in la, ∃ᶠ y in lb, p x y) :
    ∃ᶠ xy in la ×ˢ lb, p xy.1 xy.2 :=
  mt (fun h ↦ by simpa only [not_frequently] using h.curry) h

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