6.28. MappingDegree.FibresFiniteUnconditional🔗

Jacobians.MappingDegree.FibresFiniteUnconditional — source

fibres_finite

Every fibre of a non-constant analytic map between compact connected complex 1-manifolds is finite (fibres_finite_statement, with no remaining hypotheses). Direct composition of fibres_finite_statement_holds_of_clopennessOfLocallyConst with clopennessOfLocallyConst_holds.

theorem fibres_finite
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type v} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y] :
    ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f →
        ∀ y : Y, (f ⁻¹' {y}).Finite