Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.image_congr

Modification history

2022-12-07 20:30

src/data/set/basic.lean

refactor(data/set/basic): move image, preimage, and range to a new file (#17842) …

Modified set.image_congr View on Github →

2018-06-30 23:04

data/set/basic.lean

refactor(data/equiv): reorganize data.equiv deps

Modified set.image_congr View on Github →

2017-12-08 08:32

data/set/lattice.lean

feat(data/dardinal): wellordering of cardinals

Added set.image_congr View on Github →