English
If two jointly continuous functions f,g : X → Y → Z agree on s × t and agree in each variable separately, then they agree on closure(s) × closure(t).
Русский
Если две частично непрерывные функции f,g : X → Y → Z совпадают на s × t и по отдельным переменным, то они совпадают на closure(s) × closure(t).
LaTeX
$$$\\forall x \\in \\overline{s}, \\forall y \\in \\overline{t}, f(x,y) = g(x,y)$, under the given continuity hypotheses.$$
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₁ : ∀ x, Continuous (f x)) (hf₂ : ∀ y, Continuous fun x => f x y) (hg₁ : ∀ x, Continuous (g x))
(hg₂ : ∀ y, Continuous fun x => g x y) : ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y :=
suffices closure s ⊆ ⋂ y ∈ closure t, {x | f x y = g x y} by simpa only [subset_def, mem_iInter]
(closure_minimal fun x hx => mem_iInter₂.2 <| Set.EqOn.closure (h x hx) (hf₁ _) (hg₁ _)) <|
isClosed_biInter fun _ _ => isClosed_eq (hf₂ _) (hg₂ _)
