Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-21 17:46 618aac90

View on Github →

feat(data/set): add set.seq (use it for the appliative.seq instance for set)

Estimated changes

Modified data/set/lattice.lean

added theorem set.image_seq

modified theorem set.mem_seq_iff

added theorem set.prod_eq_seq

added theorem set.prod_image_seq_comm

added theorem set.pure_def

added def set.seq

added theorem set.seq_def

added theorem set.seq_eq_set_seq

added theorem set.seq_mono

added theorem set.seq_seq

added theorem set.seq_singleton

added theorem set.seq_subset

added theorem set.singleton_seq