K : Type u_1
E : Type ?u.115606
inst✝ : IsROrC K
⊢ 1 ≤ ‖LinearMap.mkContinuous reLm 1 (_ : ∀ (x : K), ‖↑reLm x‖ ≤ 1 * ‖x‖)‖
K : Type u_1
E : Type ?u.115606
inst✝ : IsROrC K
⊢ ‖reClm‖ = 1
apply le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _)
case h.e'_3
K : Type u_1
E : Type ?u.115606
inst✝ : IsROrC K
⊢ 1 = ‖↑reClm 1‖ / ‖1‖
K : Type u_1
E : Type ?u.115606
inst✝ : IsROrC K
⊢ 1 ≤ ‖LinearMap.mkContinuous reLm 1 (_ : ∀ (x : K), ‖↑reLm x‖ ≤ 1 * ‖x‖)‖
convert ContinuousLinearMap.ratio_le_op_norm (reClm : K →L[ℝ] ℝ) (1 : K)
no goals
case h.e'_3
K : Type u_1
E : Type ?u.115606
inst✝ : IsROrC K
⊢ 1 = ‖↑reClm 1‖ / ‖1‖
simp