def MagicFunction.Parametrisations.z₁ (t : ↑(Set.Icc 0 1)) : ℂ

Equations

• MagicFunction.Parametrisations.z₁ t = -1 + Complex.I * ↑↑t

def MagicFunction.Parametrisations.z₁' (t : ℝ) : ℂ

Equations

• MagicFunction.Parametrisations.z₁' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₁ t

def MagicFunction.Parametrisations.z₂ (t : ↑(Set.Icc 0 1)) : ℂ

Equations

• MagicFunction.Parametrisations.z₂ t = -1 + ↑↑t + Complex.I

def MagicFunction.Parametrisations.z₂' (t : ℝ) : ℂ

Equations

• MagicFunction.Parametrisations.z₂' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₂ t

def MagicFunction.Parametrisations.z₃ (t : ↑(Set.Icc 0 1)) : ℂ

Equations

• MagicFunction.Parametrisations.z₃ t = 1 + Complex.I * ↑↑t

def MagicFunction.Parametrisations.z₃' (t : ℝ) : ℂ

Equations

• MagicFunction.Parametrisations.z₃' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₃ t

def MagicFunction.Parametrisations.z₄ (t : ↑(Set.Icc 0 1)) : ℂ

Equations

• MagicFunction.Parametrisations.z₄ t = 1 - ↑↑t + Complex.I

def MagicFunction.Parametrisations.z₄' (t : ℝ) : ℂ

Equations

• MagicFunction.Parametrisations.z₄' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₄ t

def MagicFunction.Parametrisations.z₅ (t : ↑(Set.Icc 0 1)) : ℂ

Equations

• MagicFunction.Parametrisations.z₅ t = Complex.I * ↑↑t

def MagicFunction.Parametrisations.z₅' (t : ℝ) : ℂ

Equations

• MagicFunction.Parametrisations.z₅' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₅ t

def MagicFunction.Parametrisations.z₆ (t : ↑(Set.Ici 1)) : ℂ

Equations

• MagicFunction.Parametrisations.z₆ t = Complex.I * ↑↑t

def MagicFunction.Parametrisations.z₆' (t : ℝ) : ℂ

Equations

• MagicFunction.Parametrisations.z₆' t = Set.IciExtend MagicFunction.Parametrisations.z₆ t

theorem MagicFunction.Parametrisations.z₁_in_upper_half_plane {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 < (z₁' t).im

theorem MagicFunction.Parametrisations.z₂_in_upper_half_plane {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 < (z₂' t).im

theorem MagicFunction.Parametrisations.z₃_in_upper_half_plane {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 < (z₃' t).im

theorem MagicFunction.Parametrisations.z₄_in_upper_half_plane {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 < (z₄' t).im

theorem MagicFunction.Parametrisations.z₅_in_upper_half_plane {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 < (z₅' t).im

theorem MagicFunction.Parametrisations.z₆_in_upper_half_plane {t : ℝ} (ht : t ∈ Set.Ioi 1) : 0 < (z₆' t).im

theorem MagicFunction.Parametrisations.z₁'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : z₁' t = -1 + Complex.I * ↑t

theorem MagicFunction.Parametrisations.z₂'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : z₂' t = -1 + ↑t + Complex.I

theorem MagicFunction.Parametrisations.z₃'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : z₃' t = 1 + Complex.I * ↑t

theorem MagicFunction.Parametrisations.z₄'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : z₄' t = 1 - ↑t + Complex.I

theorem MagicFunction.Parametrisations.z₅'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : z₅' t = Complex.I * ↑t

theorem MagicFunction.Parametrisations.z₆'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Ici 1) : z₆' t = Complex.I * ↑t