Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-25 15:44 bedb810b

View on Github →

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

feat(*): a few more theorems about unique and subsingleton
Fix compile, fix two non-terminate simps
Update src/topology/metric_space/antilipschitz.lean This lemma will go to another PR

Estimated changes

Modified src/data/equiv/basic.lean

Modified src/data/set/basic.lean

added theorem set.subsingleton_univ

added theorem subsingleton.eq_univ_of_nonempty

added theorem subsingleton.set_cases

Modified src/logic/unique.lean

added theorem function.injective.comap_subsingleton

added def function.surjective.unique

added theorem nonempty_unique_or_exists_ne

added theorem subsingleton_or_exists_ne

deleted def unique.of_surjective

Modified src/topology/basic.lean

added theorem subsingleton.is_closed

added theorem subsingleton.is_open

Modified src/topology/metric_space/antilipschitz.lean

added theorem antilipschitz_with.of_subsingleton