Commit 2026-03-21 06:41 2c1b2e63

View on Github →

feat(Geometry/Convex/Cone): lemmas for PointedCone.dual (#35323) Add several useful lemmas for PointedCone.dual in preparation for duality theory for FG cones. Some other changes are:

  • renamed dual_le_dual to dual_anti and added partner lemma dual_antitone
  • removed TODO comment since the stated lemma is not sufficient to prove the claim, an also this has now been proven and will become a PR in the near future.

Estimated changes

added theorem PointedCone.dual_anti
added theorem PointedCone.dual_image
added theorem PointedCone.dual_ker
deleted theorem PointedCone.dual_le_dual
added theorem PointedCone.dual_neg
added theorem PointedCone.dual_sup