English
For a function f: α × α → β, Tendsto f along x × x to y holds iff for every neighborhood W ∈ y there exists U ∈ x with f(x,x′) ∈ W for all x,x′ ∈ U.
Русский
Для функции f: α × α → β верно: Tendsto f (x ×ˢ x) y эквивалентно тому, что для каждого окрестности W ∈ y существует U ∈ x такое, что для всех x,x′ ∈ U выполняется f(x,x′) ∈ W.
LaTeX
$$$\\mathrm{Tendsto}\\,f\\,(x \\timesˢ x)\\,y \\;\\iff\\; \\forall W \\in y,\\; \\exists U \\in x,\\; \\forall x, x' : \\alpha,\\; x ∈ U \\rightarrow x' ∈ U \\rightarrow f(x,x') ∈ W$$$
Lean4
theorem tendsto_prod_self_iff {f : α × α → β} {x : Filter α} {y : Filter β} :
Filter.Tendsto f (x ×ˢ x) y ↔ ∀ W ∈ y, ∃ U ∈ x, ∀ x x' : α, x ∈ U → x' ∈ U → f (x, x') ∈ W := by
simp only [tendsto_def, mem_prod_same_iff, prod_sub_preimage_iff]
