Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.pure_def

Modification history

2022-01-09 13:09
src/data/set/functor.lean
split(data/set/functor): Split off `data.set.lattice` (#11327) …
Modified set.pure_defView on Github →
2018-10-10 03:01
data/set/lattice.lean
fix(data/set/lattice): fixing simp lemmas for set monad
Modified set.pure_defView on Github →
2018-09-21 17:46
data/set/lattice.lean
feat(data/set): add set.seq (use it for the appliative.seq instance for set)
Added set.pure_defView on Github →