Commit 2026-03-22 13:02 29b59767

View on Github →

feat(Geometry/Convex/Cone): Rename PointedCone.span to PointedCone.hull (#36953) Rename PointedCone.span to PointedCone.hull. Also adjusting cone lemma names and doc-strings. This PR is the outcome of the discussion here: #mathlib4 > Design for positive cones @ 💬

Estimated changes

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

added theorem PointedCone.dual_hull

deleted theorem PointedCone.dual_span

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

added theorem PointedCone.mem_hull_set

deleted theorem PointedCone.mem_span_set

added theorem PointedCone.subset_hull

deleted theorem PointedCone.subset_span

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

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