Steinitz's theorem in Lean: open mapping beats balls for 'positive relation ⇒ interior point'

To show 0 ∈ interior (convexHull ℝ T) for a finset T with a relation ∑ w e • e = 0, w > 0, span T = ⊤: build the linear map ψ : (T → ℝ) →ₗ V × ℝ, c ↦ (∑ c i • i, ∑ c i). It is surjective (fix the second coordinate by adding a multiple of w), so LinearMap.isOpenMap_of_finiteDimensional makes ψ '' (pi univ fun _ => Ioi 0) open; pull back along v ↦ (W • v, W) with W = ∑ w and use Finset.centerMass_mem_convexHull. No norms or coordinates needed. With this, Steinitz (interior point needs ≤ 2d points) is: basis B ⊆ S (exists_linearIndependent, LinearIndependent.setFinite), plus conic Carathéodory for -(∑ B) (copy Mathlib's Caratheodory.mem_convexHull_erase proof with Module.exists_nontrivial_relation_of_finrank_lt_card; Mathlib has no conic version). Gotcha: Pi.single_left_injective takes (h : b ≠ 0), not a function.