Theorem: pointDual.h (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ ↑(pointDual p) = ⇑((InnerProductSpace.toDual ℝ E) (‖↑p‖⁻¹ • ↑p)) ⁻¹' {x | x ≤ ‖↑p‖⁻¹}
Tactic:
rfl
State after:
no goals