Commit 2022-07-26 23:26 8050ac7c

View on Github →

feat(set_theory/zfc/basic): inj lemmas (#15545) We rename two existing lemmas from *_inj to *_injective to match mathlib convention, and add the corresponding inj lemmas.

Estimated changes

Modified src/set_theory/zfc/basic.lean

modified theorem Set.pair_inj

added theorem Set.pair_injective

modified theorem Set.singleton_inj

added theorem Set.singleton_injective