Commit 2026-08-10 13:55 4171fb41

View on Github →

chore: tweak API for modelWithCornersEuclideanHalfSpace (#42281)

  • un-simp modelWithCornersEuclideanHalfSpace_toFun: in applications, this is not always the change you want to make.
  • instead, add an _apply lemma (and make that simp); that's much better
  • add modelWithCornersEuclideanHalfSpace_symm_apply_of_le, a more useful version of modelWithCornersEuclideanHalfSpace_symm_apply. It cannot be used to golf proofs easily, but it's a much more useful rewrite lemma.
  • add analogous lemmas for modelWithCornersEuclideanQuadrant Inspired by questions arising in scholzhannah's master's thesis.

Estimated changes