Theorem: Convex_cutSpace (src/Cutspace.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ Convex ℝ (cutSpace H_)
Tactic:
apply convex_sInter
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ ∀ s ∈ SetLike.coe '' H_, Convex ℝ s

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
⊢ ∀ s ∈ SetLike.coe '' H_, Convex ℝ s
Tactic:
rintro _ ⟨ Hi_, _, rfl ⟩
State after:
case h.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ Convex ℝ ↑Hi_

State before:
case h.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ Convex ℝ ↑Hi_
Tactic:
exact Halfspace_convex Hi_
State after:
no goals