Commit 2022-03-12 16:17 7e5ac6ad

View on Github →

chore(analysis/convex/strict): Reduce typeclass assumptions, golf (#12627) Move lemmas around so they are stated with the correct generality. Restate theorems using pointwise operations. Golf proofs. Fix typos in docstrings.

Estimated changes

Modified src/analysis/convex/strict.lean

modified theorem strict_convex.add

modified theorem strict_convex.add_left

modified theorem strict_convex.add_right

modified theorem strict_convex.affinity

modified theorem strict_convex.linear_image

modified theorem strict_convex.smul

added theorem strict_convex.vadd