Commit 2022-12-06 19:52 21bd5f5a

View on Github →

feat: port Data.Sigma.Order (#887) mathlib3 SHA: 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a porting notes: smooth, but there was one instance here and in Data.PSigma.Order that was wrong because it was wrong in mathlib3. Since that instance (apparently) never got used in mathlib3 I haven't bothered to make a mathlib3 PR to fix it, and instead I have just fixed it here.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/PSigma/Order.lean

Created Mathlib/Data/Sigma/Order.lean

added theorem Sigma.Lex.le_def

added theorem Sigma.Lex.lt_def

added theorem Sigma.le_def

added theorem Sigma.lt_def

added theorem Sigma.mk_le_mk_iff

added theorem Sigma.mk_lt_mk_iff