English
If a function f:X×Y→Z is continuous in two variables and maps s×t into a set u, then (f x y) ∈ closure(u) whenever x∈closure(s) and y∈closure(t).
Русский
Если функция f непрерывна по двум переменным и отображает s×t в u, то f(x,y) ∈ closure(u) при x∈closure(s) и y∈closure(t).
LaTeX
$$$$\text{If }\mathrm{Continuous}(\mathrm{uncurry}\,f)\text{ and }x\in\overline{s},\ y\in\overline{t},\ \forall a\in s,\forall b\in t:\ f(a,b) \in u \Rightarrow f(x,y) \in \overline{u}.$$$$
Lean4
theorem map_mem_closure₂ {f : X → Y → Z} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z}
(hf : Continuous (uncurry f)) (hx : x ∈ closure s) (hy : y ∈ closure t) (h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u) :
f x y ∈ closure u :=
have H₁ : (x, y) ∈ closure (s ×ˢ t) := by simpa only [closure_prod_eq] using mk_mem_prod hx hy
have H₂ : MapsTo (uncurry f) (s ×ˢ t) u := forall_prod_set.2 h
H₂.closure hf H₁
