fta_winding_homotopy_preserves_lift

Proved

by Henry Yuen · May 22, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Continuous liftability is preserved under circle homotopy.

Preamble

import Definitions.Def_fta_winding_infra

Formal statement


theorem fta_winding_homotopy_preserves_lift (γ δ : FtaCircle → Circle)
    (hhom : FtaCircleHomotopic γ δ) (hlift : FtaHasLift γ) :
    FtaHasLift δ := by
  sorry

Source

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/Polynomial/Basic.html#Complex.exists_root

View graph