Theorems · Theorem · complex analysis

Complex.eqOn_closure_of_eqOn_frontier

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [Nontrivial E] {f g : E → F} {U : Set E},
  Bornology.IsBounded U → DiffContOnCl ℂ f U → DiffContOnCl ℂ g U → Set.EqOn f g (frontier U) → Set.EqOn f g (closure U)

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.

Defined in

Mathlib.Analysis.Complex.AbsMax

Cited by

1 results in Mathlib

Foundations

Depth 291 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNontrivial