case intro
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
⊢ Metric.Bounded (polar 𝕜 s)
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
⊢ Metric.Bounded (polar 𝕜 s)
obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜
case intro.intro.intro
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
r : ℝ
r_pos : 0 < r
r_ball : ball 0 r ⊆ s
⊢ Metric.Bounded (polar 𝕜 s)
case intro
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
⊢ Metric.Bounded (polar 𝕜 s)
obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhd
no goals
case intro.intro.intro
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
r : ℝ
r_pos : 0 < r
r_ball : ball 0 r ⊆ s
⊢ Metric.Bounded (polar 𝕜 s)
exact
  bounded_closedBall.mono
    (((dualPairing 𝕜 E).flip.polar_antitone r_ball).trans <|
      polar_ball_subset_closedBall_div ha r_pos)