English
If two complex-differentiable functions f and g on a bounded set U agree on the frontier of U, then they agree on U itself.
Русский
Пусть две комплексно дифференцируемые функции f и g на ограниченном множестве U совпадают на границе U; тогда они совпадают и внутри U.
LaTeX
$$$$\forall f,g: E \to F,\forall U \subset E, \operatorname{IsBounded}(U) \land \operatorname{DiffContOnCl}(\mathbb{C}, f, U) \land \operatorname{DiffContOnCl}(\mathbb{C}, g, U) \land f = g \text{ on } \partial U \Rightarrow f = g \text{ on } 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 `U`. -/
theorem eqOn_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 U :=
(eqOn_closure_of_eqOn_frontier hU hf hg hfg).mono subset_closure
