Theorem: polarDual_comm (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Y : Set E
⊢ X ⊆ polarDual Y ↔ Y ⊆ polarDual X
Tactic:
constructor <;> exact fun h => polarDual_comm_half _ _ h
State after:
no goals