English
If hp, hq relate eventualities in f×g and g×h respectively, and hpqr relates p,q,r, then eventually r holds in f×h.
Русский
Если hp, hq задают конечные свойства в f×g и g×h соответственно, и hpqr связывает p, q, r, тогда в итоге для f×h выполняется r.
LaTeX
$$$\forall f,g,h\, (hp : \mathrm{Eventual}\ (p)\ f g)\, (hq : \mathrm{Eventual}\ (q)\ g h)\, (hpqr : \forall x y z, p x y \to q y z \to r x z) \Rightarrow \, \mathrm{Eventual}\ (\lambda xz. r x z.1 z.2) (f × h)$$$
Lean4
/-- A technical lemma which is a generalization of `Filter.Eventually.trans_prod`. -/
theorem eventually_prod_of_eventually_swap {h : Filter γ} [NeBot g] {p : α → β → Prop} {q : β → γ → Prop}
{r : α → γ → Prop} (hp : ∀ᶠ x in f, ∀ᶠ y in g, p x y) (hq : ∀ᶠ z in h, ∀ᶠ y in g, q y z)
(hpqr : ∀ x y z, p x y → q y z → r x z) : ∀ᶠ xz in f ×ˢ h, r xz.1 xz.2 :=
by
refine eventually_prod_iff.mpr ⟨_, hp, _, hq, fun {x} hx {z} hz ↦ ?_⟩
rcases (hx.and hz).exists with ⟨y, hpy, hqy⟩
exact hpqr x y z hpy hqy
