mathlib3
feat(data/fintype): prove `card (subtype p) ≤ card α`
#1383

Merged

feat(data/fintype): prove `card (subtype p) ≤ card α` #1383

ChrisHughes24 merged 6 commits into leanprover-community:master from urkud:card-subtype-le

feat(data/fintype): prove `card (subtype p) ≤ card α`

8f4a2734

urkud requested a review 6 years ago

jcommelin commented on 2019-09-02

Add `cardinal.mk_le_of_subtype`

7d56ba1e

Merge branch 'master' into card-subtype-le

d86098dc

Merge branch 'master' into card-subtype-le

a51ec10e

rwbarton commented on 2019-09-02

Rename `mk_le_of_subtype` to `mk_subtype_le`, use it in `mk_set_le`

25b27cbc

Merge branch 'master' into card-subtype-le

86716cf6

ChrisHughes24 approved these changes on 2019-09-03

ChrisHughes24 merged 94205c46 into master 6 years ago

urkud deleted the card-subtype-le branch 6 years ago

Reviewers

ChrisHughes24

rwbarton

jcommelin

Assignees

No one assigned

Labels

None yet

Milestone

No milestone