Commit 2024-02-22 15:18 ae19d826

View on Github →

feat: Some constructions about RelSeries (reverse, snoc, cons, tail, smash) (#3852)

reverse a RelSeries to give another RelSeries of the opposite relation
cons: put a smaller element in the front
snoc: put a larger element in the end
tail: chop off the first element
eraseLast: chop off the last element
smash: glue two relation series togather

Estimated changes

Modified Mathlib/Order/RelSeries.lean

added theorem RelSeries.append_apply_left

added theorem RelSeries.append_apply_right

added def RelSeries.cons

added def RelSeries.eraseLast

added theorem RelSeries.head_append

added theorem RelSeries.head_cons

added theorem RelSeries.head_eraseLast

added theorem RelSeries.head_smash

added theorem RelSeries.head_tail

added theorem RelSeries.last_append

added theorem RelSeries.last_cons

added theorem RelSeries.last_eraseLast

added theorem RelSeries.last_smash

added theorem RelSeries.last_tail

added theorem RelSeries.map_apply

added def RelSeries.reverse

added theorem RelSeries.reverse_apply

added def RelSeries.smash

added theorem RelSeries.smash_castAdd

added theorem RelSeries.smash_natAdd

added theorem RelSeries.smash_succ_castAdd

added theorem RelSeries.smash_succ_natAdd

added def RelSeries.tail