English
Let p : α × β → Prop. Then p holds eventually on the product f × g if and only if there exist predicates pa : α → Prop and pb : β → Prop such that pa holds frequently in f, pb holds frequently in g, and for all x,y with pa x and pb y we have p(x,y).
Русский
Пусть p : α × β → Prop. Тогда p выполняется eventually на произведении f × g тогда и только тогда, когда существуют предикаты pa : α → Prop и pb : β → Prop, такие что pa часто выполняется в f, pb часто выполняется в g, и для всех x,y с pa x и pb y выполняется p(x,y).
LaTeX
$$$$(\forall^\infty x \in f \times g, p x) \iff \exists pa:\alpha\to\text{Prop}, (\forall^\infty x \in f, pa\,x) \land \exists pb:\beta\to\text{Prop}, (\forall^\infty y \in g, pb\,y) \land \forall {x}, pa\,x \to \forall {y}, pb\,y \to p(x,y).$$$$
Lean4
theorem eventually_prod_iff {p : α × β → Prop} :
(∀ᶠ x in f ×ˢ g, p x) ↔
∃ pa : α → Prop, (∀ᶠ x in f, pa x) ∧ ∃ pb : β → Prop, (∀ᶠ y in g, pb y) ∧ ∀ {x}, pa x → ∀ {y}, pb y → p (x, y) :=
by simpa only [Set.prod_subset_iff] using @mem_prod_iff α β p f g
