Theorem: ContinuousOn.rectangleBorder_integrable (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (RectangleBorder z w)
⊢ ContinuousOn (fun x => ↑x + ↑z.im * I) [[z.re, w.re]]
Tactic:
fun_prop
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (RectangleBorder z w)
⊢ ContinuousOn (fun x => ↑x + ↑w.im * I) [[z.re, w.re]]
Tactic:
fun_prop
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (RectangleBorder z w)
⊢ ContinuousOn (fun y => ↑w.re + ↑y * I) [[z.im, w.im]]
Tactic:
fun_prop
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (RectangleBorder z w)
⊢ ContinuousOn (fun y => ↑z.re + ↑y * I) [[z.im, w.im]]
Tactic:
fun_prop
State after:
no goals