Commit 2022-01-09 13:09 9c224ff6

View on Github →

split(data/set/functor): Split off data.set.lattice (#11327) This moves the functor structure of set in a new file data.set.functor. Also adds alternative set because it's quick and easy.

Estimated changes

Modified src/computability/NFA.lean

Modified src/control/traversable/instances.lean

Modified src/data/set/finite.lean

Created src/data/set/functor.lean

added theorem set.bind_def

added theorem set.fmap_eq_image

added theorem set.pure_def

added theorem set.seq_eq_set_seq

Modified src/data/set/lattice.lean

deleted theorem set.bind_def

deleted theorem set.fmap_eq_image

deleted theorem set.pure_def

deleted theorem set.seq_eq_set_seq