English
A product-level tendsto criterion: Tendsto f (x ×ˢ y) z is equivalent to a quantified condition over z: for every W ∈ z, there exist U ∈ x and V ∈ y such that for all x ∈ U and y ∈ V, f(x,y) ∈ W.
Русский
Критерий сходимости по произведению: Tendsto f (x × y) z эквивалентен тому, что для каждого W ∈ z существуют U ∈ x, V ∈ y, такие что для всех x ∈ U и y ∈ V, f(x,y) ∈ W.
LaTeX
$$$ \\operatorname{Tendsto} f (x \\times\\! y) z \\iff \\forall W \\in z, \\exists U \\in x, \\exists V \\in y, \\forall x \\in U, \\forall y \\in V, f(x,y) \\in W $$$
Lean4
theorem tendsto_prod_iff {f : α × β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} :
Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ x y, x ∈ U → y ∈ V → f (x, y) ∈ W := by
simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff]
