Removable lines for holomorphic functions

DefinitionReal axis#✓fully proved

The real axis is the set \(\{z \in \mathbb{C} : \operatorname{Im} z = 0\}\).

def realAxis : Set ℂ := {z : ℂ | z.im = 0}

Used by 1

Used byCoordinate axes

DefinitionImaginary axis#✓fully proved

The imaginary axis is the set \(\{z \in \mathbb{C} : \operatorname{Re} z = 0\}\).

def imagAxis : Set ℂ := {z : ℂ | z.re = 0}

Used by 1

Used byCoordinate axes

DefinitionCoordinate axes#✓fully proved

The coordinate axes of \(\mathbb{C}\): the union of the real axis and the imaginary axis.

def coordAxes : Set ℂ := realAxis ∪ imagAxis

Uses 2 · Used by 1

Statement usesImaginary axis · Real axis

Used byContinuous functions holomorphic off the coordinate axes are entire

TheoremContinuous functions holomorphic off the coordinate axes are entire#●ready to prove

Let \(f : \mathbb{C} \to \mathbb{C}\) be continuous on all of \(\mathbb{C}\) and holomorphic on the complement of the coordinate axes. Then \(f\) is holomorphic on all of \(\mathbb{C}\).

public theorem_wanted differentiable_of_continuous_of_differentiableOn_compl_coordAxes
    (f : ℂ → ℂ) (hc : Continuous f) (hhol : DifferentiableOn ℂ f (coordAxesᶜ)) :
    Differentiable ℂ f

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l1_27.

Uses 1

Statement usesCoordinate axes

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.