feat: simple lemmas about LE and LT #372
Conversation
semorrison
added
the
awaiting-review
|
|
||
| @[simp] theorem gt_iff_lt [LT α] {x y : α} : x > y ↔ y < x := Iff.rfl | ||
|
|
||
| theorem le_of_eq_of_le {a b c : α} [LE α] (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c := by subst h₁; exact h₂ |
There was a problem hiding this comment.
These have dot notation aliases as well in mathlib (e.g. Eq.trans_le). How do you feel about adding those?
There was a problem hiding this comment.
I'm not convinced they make sense without also upstreaming the primed versions e.g. le_of_eq_of_le', we could have Eq.trans_ge as well as Eq.trans_le.
(Edit: on second thoughts, done!)
More generally, I think with upstreaming PRs the right course of action instead of proposing "how about also upstreaming these?" is to make a second PR. I'd prefer to be able to move stuff that I know I need, without necessarily having to have a discussion about how much more to move at the same time.
There's also the danger of upstreaming cruft from Mathlib that isn't actually going to be used. :-)
There was a problem hiding this comment.
Eq.trans_le/Eq.trans_lt are both special cases of Eq.substr. I don't think we need to clutter the Eq namespace with special cases of Eq.subst/Eq.substr.
There was a problem hiding this comment.
I can see the utility for .trans_eq but I would prefer .congr_right or similar since I can't think of a precedent for trans_eq in std or core.
There was a problem hiding this comment.
There's no way I'm going to include in this PR a lemma I don't care about, moved from Mathlib, but changing it's name.
As there is needless controversy, I'm removing the aliases from this PR. If someone needs them in Std, or has opinions about their names in Mathlib, please PR those separately!
No description provided.