Theorem: Vpolytope_translation (src/Polytope.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set E
hS : Set.Finite S
x : E
⊢ Vpolytope ⋯ = Vpolytope hS + {x}
Tactic:
rw [Vpolytope, convexHull_add, convexHull_singleton]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set E
hS : Set.Finite S
x : E
⊢ (convexHull ℝ) S + {x} = Vpolytope hS + {x}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set E
hS : Set.Finite S
x : E
⊢ (convexHull ℝ) S + {x} = Vpolytope hS + {x}
Tactic:
rfl
State after:
no goals