Commit 2022-11-03 02:45 7901e76c

View on Github →

feat: port Logic.Unique (#512)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Init/Data/Fin/Basic.lean

added theorem Fin.eq_of_veq

added theorem Fin.ne_of_vne

added theorem Fin.veq_of_eq

added theorem Fin.vne_of_ne

Modified Mathlib/Logic/IsEmpty.lean

Created Mathlib/Logic/Unique.lean

added theorem Fin.default_eq_zero

added theorem Fin.eq_zero

added def Function.Surjective.uniqueOfSurjectiveConst

added theorem Option.subsingleton_iff_is_empty

added theorem PUnit.default_eq_unit

added theorem Pi.default_apply

added theorem Pi.default_def

added theorem Unique.bijective

added theorem Unique.default_eq

added theorem Unique.eq_default

added theorem Unique.exists_iff

added theorem Unique.forall_iff

added def Unique.mk'

added structure Unique

added theorem eq_const_of_unique

added theorem heq_const_of_unique

added def uniqueOfSubsingleton

added def uniqueProp

added theorem unique_iff_exists_unique

added theorem unique_iff_subsingleton_and_nonempty

added theorem unique_subtype_iff_exists_unique

Modified Mathlib/Tactic/Inhabit.lean

Modified test/Inhabit.lean

added def Unique.mk'

added structure Unique