[Merged by Bors] - feat(data/fintype/basic): add card_subtype_mono
#14645
Conversation
linesthatinterlace
changed the title
card_subtype_le_of_imp
linesthatinterlace
added
awaiting-review
|
Note that if you repeat the PR title in the PR description, it will appear in the commit message twice (so don't do that!) |
| @@ -1456,6 +1456,11 @@ begin | |||
| intro; simp only [set.mem_to_finset, set.mem_compl_eq]; refl, | |||
| end | |||
|
|
|||
| theorem card_subtype_le_of_imp (p q : α → Prop) (h : p ≤ q) | |||
| [fintype {x // p x}] [fintype {x // q x}] : | |||
| fintype.card {x // p x} ≤ fintype.card {x // q x} := | |||
There was a problem hiding this comment.
Do we have the cardinal.mk version of this already?
There was a problem hiding this comment.
Ah yes, it's cardinal.mk_subtype_mono
So I think this should be called fintype.card_subtype_mono to match.
There was a problem hiding this comment.
This makes sense, though I wonder if that means that subtype.imp_embedding should also be changed to something like subtype.embedding_mono?
There was a problem hiding this comment.
Well, or indeed subtype_embedding_mono?
There was a problem hiding this comment.
This lemma is called mono because it has a ≤ both in its conclusion and its aassumptions. subtype.imp_embedding does not match this pattern.
There was a problem hiding this comment.
Right, that makes sense. Do you agree with my renaming of subtype.imp_embedding to subtype_imp_embedding? I couldn't work out why it was as it was.
There was a problem hiding this comment.
I think the old name was probably better; it matches things like subtype.coind.
There was a problem hiding this comment.
Hmm - but there are a number of subtype_ lemmas also. What's the rationale for why one is one and not the other?
There was a problem hiding this comment.
I'm not really sure, but in situations like this where things are already inconsistent, renaming just one lemma is just noise which might makes things better or might make things worse; so better to stick with the status quo and not repaint fractional bikesheds.
You could start a zulip thread, but I think this is one of those cases where no one really cares, and also where your time would be much better invested into developing your crypto / hamming stuff
There was a problem hiding this comment.
I've removed the name change you thought wasn't a good idea, and done the one that you said was.
github-actions
bot
removed
the
awaiting-CI
bryangingechen
changed the title
card_subtype_le_of_impcard_subtype_le_of_imp
bryangingechen
changed the title
card_subtype_le_of_impcard_subtype_le_of_imp
linesthatinterlace
force-pushed
the
card_subtype_le_of_imp
branch
from
33be93e
to
936e5d3
Compare
linesthatinterlace
changed the title
card_subtype_le_of_impcard_subtype_mono
linesthatinterlace
added
the
awaiting-CI
|
bors d+ Thanks! |
|
✌️ linesthatinterlace can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
|
👎 Rejected by label |
github-actions
bot
removed
the
awaiting-CI
|
bors r+ |
This lemma naturally forms a counterpart to existing lemmas. I've also renamed a lemma it uses that didn't seem to fit the existing naming pattern.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
card_subtype_monocard_subtype_mono
This lemma naturally forms a counterpart to existing lemmas.
I've also renamed a lemma it uses that didn't seem to fit the existing naming pattern.
We were missing this which was a fairly straightforward lemma, so I added it (and edited a lemma name that looked misnamed).