Commit 2023-06-09 14:00 02341406

View on Github →

feat: port Analysis.NormedSpace.AddTorsorBases (#4903)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/AddTorsorBases.lean

added theorem AffineBasis.centroid_mem_interior_convexHull

added theorem AffineBasis.interior_convexHull

added theorem Convex.interior_nonempty_iff_affineSpan_eq_top

added theorem IsOpen.affineSpan_eq_top

added theorem IsOpen.exists_between_affineIndependent_span_eq_top

added theorem IsOpen.exists_subset_affineIndependent_span_eq_top

added theorem affineSpan_eq_top_of_nonempty_interior

added theorem continuous_barycentric_coord

added theorem interior_convexHull_nonempty_iff_affineSpan_eq_top

added theorem isOpenMap_barycentric_coord

added theorem smooth_barycentric_coord