Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.inj_on.ne_iff

Modification history

2022-10-03 08:59

src/data/set/function.lean

feat(data/fintype/basic): Existence of a bijection with specified behaviour on a subset (#16479) …

Added set.inj_on.ne_iff View on Github →