Commit 2025-04-28 14:59 c768c54c

View on Github →

chore(Analysis/Convex): drop unused arguments (#24392) Also weaken typeclass assumptions here and there.

Estimated changes

modified theorem Convex.starConvex_iff
modified theorem Set.OrdConnected.convex
modified theorem convex_segment
modified theorem convex_stdSimplex
modified theorem stdSimplex_unique
modified def affineSegment
modified theorem List.sbtw_cons
modified theorem List.sbtw_four
modified theorem List.sbtw_triple
modified theorem convexHull_pair
modified theorem Set.OrdConnected.starConvex
modified theorem StarConvex.mem
modified def StarConvex
modified theorem StrictConvex.add_smul_mem
modified def StrictConvex
modified theorem IsVisible.rfl
modified theorem isVisible_comm