theorem isOpen_affineIndependent (𝕜 : Type u_1) (E : Type u_2) {ι : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] [Finite ι] : IsOpen {p : ι → E | AffineIndependent 𝕜 p}