Theorem: Halfspace_closed (src/Halfspace.lean)

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

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Halfspace E
⊢ IsClosed (⇑↑H_.f ⁻¹' {x | x ≤ H_.α})
Tactic:
exact IsClosed.preimage (H_.f.1.cont) isClosed_Iic
State after:
no goals