Theorem: mem_polarDual' (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
v : E
⊢ v ∈ polarDual X ↔ ∀ x ∈ X, ⟪v, x⟫_ℝ ≤ 1
Tactic:
simp_rw [mem_polarDual, real_inner_comm]
State after:
no goals