Theorem: Hyperplane_convex (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
Hi_ : Halfspace E
⊢ Convex ℝ {x | ↑Hi_.f x = Hi_.α}
Tactic:
exact @convex_hyperplane ℝ E ℝ _ _ _ _ _ _ Hi_.f.1 (LinearMap.isLinear Hi_.f.1) Hi_.α
State after:
no goals