Theorem: Hpolytope.I_sub (src/MainTheorem.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ I H_ x ⊆ H_
Tactic:
unfold Hpolytope.I
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ {Hi_ | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_} ⊆ H_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ {Hi_ | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_} ⊆ H_
Tactic:
simp only [Set.sep_subset]
State after:
no goals