Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.mem_range_self

Modification history

2023-06-30 11:29
src/data/set/image.lean
refactor(*): move all `mk_simp_attribute` commands to 1 file (#19223)
Modified set.mem_range_selfView on Github →
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.mem_range_selfView on Github →
2020-07-01 10:05
src/data/set/basic.lean
chore(data/set/basic): simp attribute on mem_range_self (#3260)
Modified set.mem_range_selfView on Github →
2017-12-31 16:53
data/set/basic.lean
feat(data/ordinal): is_normal, omin, power/log, CNF, indecomposables, …
Modified set.mem_range_selfView on Github →
2017-12-17 02:45
data/set/basic.lean
feat(data/ordinal): ordinal collapse, ordinals ordering,
Added set.mem_range_selfView on Github →