Theorem: Convex_Hpolytope (src/Polytope.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ Convex ℝ (Hpolytope hH_)
Tactic:
apply convex_sInter
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ ∀ 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)
hH_ : Set.Finite H_
⊢ ∀ 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)
hH_ : Set.Finite H_
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)
hH_ : Set.Finite H_
Hi_ : Halfspace E
left✝ : Hi_ ∈ H_
⊢ Convex ℝ ↑Hi_
Tactic:
exact Halfspace_convex Hi_
State after:
no goals