case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖

case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
by_cases z_zero : z = 0
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
set z₁ := ((r : 𝕜) * (‖z‖ : 𝕜)⁻¹) • z with hz₁
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
have norm_f_z₁ : ‖f z₁‖ ≤ c := by
  apply h
  rw [mem_sphere_zero_iff_norm]
  exact norm_smul_inv_norm' r_pos.le z_zero
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
have r_ne_zero : (r : 𝕜) ≠ 0 := IsROrC.ofReal_ne_zero.mpr r_pos.ne'
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
have eq : f z = ‖z‖ / r * f z₁ := by
  rw [hz₁, LinearMap.map_smul, smul_eq_mul]
  rw [← mul_assoc, ← mul_assoc, div_mul_cancel _ r_ne_zero, mul_inv_cancel, one_mul]
  simp only [z_zero, IsROrC.ofReal_eq_zero, norm_eq_zero, Ne.def, not_false_iff]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z₁‖ * ‖z‖ / r ≤ c * ‖z‖ / r
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
rw [eq, norm_mul, norm_div, IsROrC.norm_coe_norm, IsROrC.norm_of_nonneg r_pos.le,
  div_mul_eq_mul_div, div_mul_eq_mul_div, mul_comm]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ 0 ≤ c * ‖z‖

𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z₁‖ * ‖z‖ ≤ c * ‖z‖
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z₁‖ * ‖z‖ / r ≤ c * ‖z‖ / r
apply div_le_div _ _ r_pos rfl.ge
no goals
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ ‖↑f z₁‖ * ‖z‖ ≤ c * ‖z‖
apply mul_le_mul norm_f_z₁ rfl.le (norm_nonneg z) ((norm_nonneg _).trans norm_f_z₁)
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖↑f 0‖ ≤ c / r * ‖0‖
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖↑f z‖ ≤ c / r * ‖z‖
rw [z_zero]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ 0 ≤ 0
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖↑f 0‖ ≤ c / r * ‖0‖
simp only [LinearMap.map_zero, norm_zero, MulZeroClass.mul_zero]
no goals
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : z = 0
⊢ 0 ≤ 0
exact le_rfl
case a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ z₁ ∈ sphere 0 r
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖↑f z₁‖ ≤ c
apply h
case a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖z₁‖ = r
case a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ z₁ ∈ sphere 0 r
rw [mem_sphere_zero_iff_norm]
no goals
case a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖z₁‖ = r
exact norm_smul_inv_norm' r_pos.le z_zero
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑f z = ↑‖z‖ / ↑r * (↑r * (↑‖z‖)⁻¹ * ↑f z)
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑f z = ↑‖z‖ / ↑r * ↑f z₁
rw [hz₁, LinearMap.map_smul, smul_eq_mul]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑‖z‖ ≠ 0
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑f z = ↑‖z‖ / ↑r * (↑r * (↑‖z‖)⁻¹ * ↑f z)
rw [← mul_assoc, ← mul_assoc, div_mul_cancel _ r_ne_zero, mul_inv_cancel, one_mul]
no goals
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑‖z‖ ≠ 0
simp only [z_zero, IsROrC.ofReal_eq_zero, norm_eq_zero, Ne.def, not_false_iff]
no goals
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), z ∈ sphere 0 r → ‖↑f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖↑f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : ↑f z = ↑‖z‖ / ↑r * ↑f z₁
⊢ 0 ≤ c * ‖z‖
exact mul_nonneg ((norm_nonneg _).trans norm_f_z₁) (norm_nonneg z)