English
For cluster maps hf and hg, there is a correspondence between curried product maps on the product filter and the product of the original maps, preserving the frequently-true relation.
Русский
Для отображений hf и hg существует соответствие между каррированной картой prodMap и произведением отображений, сохраняющее отношение часто встречающихся.
LaTeX
$$$$ \\text{curry\\_prodMap} \\;: \\; MapClusterPt x \\; la \\; f \\; \\to\\; MapClusterPt (x,y) (la.curry lb) (Prod.map f g) $$$$
Lean4
theorem curry_prodMap {α β : Type*} {f : α → X} {g : β → Y} {la : Filter α} {lb : Filter β} {x : X} {y : Y}
(hf : MapClusterPt x la f) (hg : MapClusterPt y lb g) : MapClusterPt (x, y) (la.curry lb) (.map f g) :=
by
rw [mapClusterPt_iff_frequently] at hf hg
rw [((𝓝 x).basis_sets.prod_nhds (𝓝 y).basis_sets).mapClusterPt_iff_frequently]
rintro ⟨s, t⟩ ⟨hs, ht⟩
rw [frequently_curry_iff]
exact (hf s hs).mono fun x hx ↦ (hg t ht).mono fun y hy ↦ ⟨hx, hy⟩
