mathlib3
feat(*): a few more theorems about `unique` and `subsingleton`
#2230

Merged

feat(*): a few more theorems about `unique` and `subsingleton` #2230

mergify merged 4 commits into master from unique-subsingleton

feat(*): a few more theorems about `unique` and `subsingleton`

c44f93a0

ChrisHughes24 commented on 2020-03-24

Fix compile, fix two non-terminate `simp`s

c8313f0e

kim-em approved these changes on 2020-03-24

urkud commented on 2020-03-24

Update src/topology/metric_space/antilipschitz.lean

7cde50ef

jcommelin approved these changes on 2020-03-25

robertylewis added ready-to-merge

Merge branch 'master' into unique-subsingleton

1b6ba00b

mergify merged bedb810b into master 6 years ago

urkud deleted the unique-subsingleton branch 6 years ago

Reviewers

jcommelin

kim-em

ChrisHughes24

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone