Commit 2024-09-02 17:15 02af5954

View on Github →

feat: Intrinsic interior of a spanning set (#16090) From LeanCamCombi

Estimated changes

Modified Mathlib/Analysis/Convex/Intrinsic.lean

added theorem intrinsicClosure_eq_closure_of_span

added theorem intrinsicClosure_univ

added theorem intrinsicFrontier_eq_frontier_of_span

added theorem intrinsicFrontier_univ

added theorem intrinsicInterior_eq_interior_of_span

added theorem intrinsicInterior_univ