LeanPool.Rupert.Equivalences.RupertEquivRupertSet

Imported Lean Pool material for LeanPool.Rupert.Equivalences.RupertEquivRupertSet.

theorem rupert_imp_rupert_set {ι : Type} [Finite ι] (v : ι → ℝ³) : IsRupert v → IsRupertSet ((convexHull ℝ) (Set.range v))

theorem rupert_set_imp_rupert {ι : Type} [Finite ι] (v : ι → ℝ³) : IsRupertSet ((convexHull ℝ) (Set.range v)) → IsRupert v

theorem rupert_iff_rupert_set {ι : Type} [Finite ι] (v : ι → ℝ³) : IsRupert v ↔ IsRupertSet ((convexHull ℝ) (Set.range v))