English
A separating left property forces the polar of the whole space to be a singleton {0}.
Русский
Разделяющее слева свойство заставляет поляр всего пространства быть одиночкой {0}.
LaTeX
$$B.polar(\mathrm{univ}) = \{0\}$$
Lean4
theorem polar_univ (h : SeparatingRight B) : B.polar Set.univ = {(0 : F)} :=
by
rw [Set.eq_singleton_iff_unique_mem]
refine ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => ?_⟩
refine norm_le_zero_iff.mp (le_of_forall_gt_imp_ge_of_dense fun ε hε => ?_)
rcases NormedField.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩
calc
‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
rw [B.map_smul, LinearMap.smul_apply, Algebra.id.smul_eq_mul, norm_mul, norm_inv, mul_inv_cancel_left₀ hc.ne']
_ ≤ ε * 1 := by gcongr; exact hy _ trivial
_ = ε := mul_one _
