mathlib3
feat(data/finset): define `finset.Ico.subset_iff`
#1574

Merged

feat(data/finset): define `finset.Ico.subset_iff` #1574

mergify merged 2 commits into master from finset_Ico_subset

feat(data/finset): define `finset.Ico.subset_iff`

97191d07

kim-em approved these changes on 2019-10-21

ChrisHughes24 approved these changes on 2019-10-21

ChrisHughes24 added ready-to-merge

Merge branch 'master' into finset_Ico_subset

9bdcdecb

mergify merged f52e952e into master 6 years ago

mergify deleted the finset_Ico_subset branch 6 years ago

Reviewers

ChrisHughes24

kim-em

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone