Theorem: Halfspace_convex (src/Halfspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Convex ℝ ↑H_
Tactic:
rw [H_.h]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Convex ℝ (⇑↑H_.f ⁻¹' {x | x ≤ H_.α})

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ Convex ℝ (⇑↑H_.f ⁻¹' {x | x ≤ H_.α})
Tactic:
exact convex_halfspace_le (LinearMap.isLinear H_.f.1.1) H_.α
State after:
no goals