LeanPool.Rupert.Equivalences.RupertEquivRupertPrime

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

theorem rupert'_imp_rupert {ι : Type} (v : ι → ℝ³) : IsRupert' v → IsRupert v

theorem rupert_imp_rupert' {ι : Type} (v : ι → ℝ³) : IsRupert v → IsRupert' v

theorem rupert_iff_rupert' {ι : Type} (v : ι → ℝ³) : IsRupert v ↔ IsRupert' v