Commit 2026-07-01 01:31 2fed563e

View on Github →

refactor(Analysis/Convex/Cone): use PointedCone in Riesz extension theorem (#37053) Change the statement of the Riesz extension theorem to take a PointedCone rather than a ConvexCone. This PR is part of a series replacing ConvexCone with PointedCone. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307

Estimated changes

Modified Mathlib/Analysis/Convex/Cone/Extension.lean

modified theorem riesz_extension

Modified Mathlib/Geometry/Convex/Cone/Pointed.lean

added theorem PointedCone.smul_mem_iff