New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: Fix name of Nat.card_mono
#8340
Conversation
This was accidentally put in the `PartENat` namespace in #8202. Also add `Set.Infinite.card_eq_zero` and fix capitalisation errors.
theorem card_uLift (α : Type*) : card (ULift α) = card α := | ||
card_congr Equiv.ulift | ||
#align part_enat.card_ulift PartENat.card_uLift | ||
|
||
@[simp] | ||
theorem card_pLift (α : Type*) : card (PLift α) = card α := | ||
card_congr Equiv.plift | ||
#align part_enat.card_plift PartENat.card_pLift | ||
@[simp] lemma card_ulift (α : Type*) : card (ULift α) = card α := card_congr Equiv.ulift | ||
#align part_enat.card_ulift PartENat.card_ulift | ||
|
||
lemma card_mono {s t : Set α} (ht : t.Finite) (h : s ⊆ t) : Nat.card s ≤ Nat.card t := | ||
toNat_le_of_le_of_lt_aleph0 ht.lt_aleph0 <| mk_le_mk_of_subset h | ||
@[simp] lemma card_plift (α : Type*) : card (PLift α) = card α := card_congr Equiv.plift | ||
#align part_enat.card_plift PartENat.card_plift |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Where did we decide PLift
should turn into plift
rather than pLift
, and what's the rationale? (From the existing names in mathlib4 indeed plift
seems to be the convention ...)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
First cluster of caps gets lowercased. That's the rule I know.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay, LGTM!
maintainer merge
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
This was accidentally put in the `PartENat` namespace in #8202. Also add `Set.Infinite.card_eq_zero` and fix capitalisation errors.
Pull request successfully merged into master. Build succeeded: |
Nat.card_mono
Nat.card_mono
This was accidentally put in the `PartENat` namespace in #8202. Also add `Set.Infinite.card_eq_zero` and fix capitalisation errors.
This was accidentally put in the `PartENat` namespace in #8202. Also add `Set.Infinite.card_eq_zero` and fix capitalisation errors.
This was accidentally put in the `PartENat` namespace in #8202. Also add `Set.Infinite.card_eq_zero` and fix capitalisation errors.
This was accidentally put in the
PartENat
namespace in #8202. Also addSet.Infinite.card_eq_zero
and fix capitalisation errors.