Commit 2025-09-02 18:26 f033e7eb

View on Github →

feat(Analysis/Convex): Lifting convex sets along scalar towers (#29075) This PR continues the work from #25637. Original PR: https://github.com/leanprover-community/mathlib4/pull/25637

Estimated changes

Modified Mathlib/Analysis/Convex/Basic.lean

deleted theorem Convex.add_smul

added theorem Convex.lift

Modified Mathlib/Analysis/Convex/Between.lean

added theorem Sbtw.lift

added theorem Wbtw.lift

added theorem affineSegment.lift

Modified Mathlib/Analysis/Convex/Segment.lean

added theorem openSegment.lift

added theorem segment.lift