𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) ⊆ closedBall 0 r⁻¹
𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) = closedBall 0 r⁻¹
refine' Subset.antisymm _ (closedBall_inv_subset_polar_closedBall 𝕜)
𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ x' ∈ closedBall 0 r⁻¹
𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) ⊆ closedBall 0 r⁻¹
intro x' h
𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ ‖x'‖ ≤ r⁻¹
𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ x' ∈ closedBall 0 r⁻¹
simp only [mem_closedBall_zero_iff]
𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
z : E
x✝ : z ∈ ball 0 r
⊢ ‖↑x' z‖ ≤ r⁻¹ * ‖z‖
𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ ‖x'‖ ≤ r⁻¹
refine' ContinuousLinearMap.op_norm_le_of_ball hr (inv_nonneg.mpr hr.le) fun z _ => _
no goals
𝕜✝ : Type ?u.142772
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type ?u.142778
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
z : E
x✝ : z ∈ ball 0 r
⊢ ‖↑x' z‖ ≤ r⁻¹ * ‖z‖
simpa only [one_div] using LinearMap.bound_of_ball_bound' hr 1 x'.toLinearMap h z