English
If two complex-differentiable functions f and g on a bounded set U coincide on the boundary frontier of U, then they coincide on the entire closure of U.
Русский
Если две комплексно дифференцируемые функции f и g на ограниченном множестве U совпадают на границе frontier(U), то они совпадают на все closures(U).
LaTeX
$$$$\forall f,g: E \to F,\forall U \subset E, \bigl( \operatorname{IsBounded}(U) \land \operatorname{DiffContOnCl}(\mathbb{C}, f, U) \land \operatorname{DiffContOnCl}(\mathbb{C}, g, U) \land f|_{\partial U} = g|_{\partial U} \bigr) \Rightarrow f|_{\overline{U}} = g|_{\overline{U}}.$$$$
Lean4
/-- If two complex differentiable functions `f g : E → F` are equal on the boundary of a bounded set
`U`, then they are equal on `closure U`. -/
theorem eqOn_closure_of_eqOn_frontier {f g : E → F} {U : Set E} (hU : IsBounded U) (hf : DiffContOnCl ℂ f U)
(hg : DiffContOnCl ℂ g U) (hfg : EqOn f g (frontier U)) : EqOn f g (closure U) :=
by
suffices H : ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0 by simpa [sub_eq_zero] using H
refine fun z hz => norm_le_of_forall_mem_frontier_norm_le hU (hf.sub hg) (fun w hw => ?_) hz
simp [hfg hw]
