English
Let X, Y, Z be topological spaces with Z Hausdorff. Suppose f, g: X → Y → Z satisfy f x y = g x y for all x in a set s ⊆ X and y in a set t ⊆ Y, and suppose f and g are continuous when viewed as functions of two variables. Then f and g agree on the product of closures, i.e. for all x ∈ closure s and y ∈ closure t, f x y = g x y.
Русский
Пусть X, Y, Z — топологические пространства, Z тахофазно-чёткое. Пусть f, g: X → Y → Z удовлетворяют f x y = g x y для всех x ∈ s ⊆ X и y ∈ t ⊆ Y, причём f и g непрерывны как функции от пары переменных. Тогда они совпадают на произведении замыканий: для всех x ∈ closure s и y ∈ closure t выполняется f x y = g x y.
LaTeX
$$$\\forall s \\subseteq X, \\forall t \\subseteq Y, \\forall f,g:X\\to Y\\to Z,\\ (\\forall x\\in s\\, \\forall y\\in t, f(x,y)=g(x,y))\\ \\land\\ hf: Continuous(uncurry(f))\\land hg: Continuous(uncurry(g))\\Rightarrow\\forall x\\in \\overline{s}, \\forall y\\in \\overline{t}, f(x,y)=g(x,y).$$$
Lean4
theorem eqOn_closure₂ [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z} (h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y)
(hf : Continuous (uncurry f)) (hg : Continuous (uncurry g)) : ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y :=
eqOn_closure₂' h hf.uncurry_left hf.uncurry_right hg.uncurry_left hg.uncurry_right
