Repository navigation
Bump mathlib - #113
Bump mathlib#113
Conversation
| @[simp] lemma map_sConvexComb (w : StdSimplex R P₁) : | ||
| f (sConvexComb w) = sConvexComb (w.map f) := f.isAffineMap.map_sConvexComb w |
There was a problem hiding this comment.
I wonder if we shouldn't remove these ones now that we have the IsAffineMap lemma
There was a problem hiding this comment.
Yes the simp lemma is not in simpNF, _image is already upstream by a different name, and a couple of these are copied for LinearMap/AffineMap. I have cleaned this up.
| /-! This files proves results about faces of convex sets / cones and homogenization. -/ | ||
|
|
||
| @[expose] public section | ||
| @[expose] public noncomputable section |
There was a problem hiding this comment.
Do we know what triggered this?
There was a problem hiding this comment.
I think this is due to mathlib refactoring Set to be a one-field structure so that now building a Set in an expression is more likely to lead to a def referencing a set to have runtime content and require being marked noncomputable. (Also because ofPoint is now noncomputable as of #102).
|
I would appreciate a PR summary, also on bumps. Otherwise it is hard to judge what changes are correct/intentional. For example, where does |
Will do, there's one now. |
|
LGTM @ooovi |
|
Thanks! :) |
5 participants
map_sConvexComb/isConvexSet_image/isConvexSet_rangecopies.map_sConvexComb/isConvexSet_imageare now upstream, keep a singleisConvexSet_range.noncomputable sectionsthat are now required, this appears to be becauseofPointis noncomputable and Set is now a 1-field structure so moredefs cause there to be computable data@[to_dual]changed, requiring adding some more(dont_translate := R)