English
A generalized product transitivity: from hp in f×g and hq in g×h, with hpqr linking p,q,r, deduce r in f×h.
Русский
Обобщенная транспозиция произведения: из hp в f×g и hq в g×h, при наличии hpqr, выводим r в f×h.
LaTeX
$$$\forall f,g,h\, (hp : \forall^\mathrm{f} xy \in f×g, p x y)\, (hq : \forall^\mathrm{f} yz \in g×h, q y z)\, (hpqr : \forall x y z, p x y \to q y z \to r x z) \Rightarrow \mathrm{Eventual}\ (\lambda xz. r x z) (f × h)$$$
Lean4
theorem trans_prod {h : Filter γ} [NeBot g] {p : α → β → Prop} {q : β → γ → Prop} {r : α → γ → Prop}
(hp : ∀ᶠ xy in f ×ˢ g, p xy.1 xy.2) (hq : ∀ᶠ yz in g ×ˢ h, q yz.1 yz.2) (hpqr : ∀ x y z, p x y → q y z → r x z) :
∀ᶠ xz in f ×ˢ h, r xz.1 xz.2 :=
hp.curry.eventually_prod_of_eventually_swap (eventually_swap_iff.mp hq |>.curry) hpqr
