Theorems · Theorem · several complex variables

MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {H : Type u_3} [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
  {M : Type u_4} [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {U : Set M}
  {a b : M}, MDiff[U] f → IsPreconnected U → IsCompact U → IsOpen U → a ∈ U → b ∈ U → f a = f b

If a function f : M → F from a complex manifold to a complex normed space is holomorphic on a (pre)connected compact open set, then it is a constant on this set.

Defined in

Mathlib.Geometry.Manifold.Complex

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceModelWithCorners.BoundarylessTopologicalSpaceChartedSpaceIsManifold