Commit 2022-12-20 13:42 db9b53ae

View on Github →

feat: port Data.Pi.Lex (#1104) mathlib3 SHA: d4f69d96f3532729da8ebb763f4bc26fcf640f06

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Pi/Lex.lean

added theorem Pi.Lex.noMaxOrder'

added theorem Pi.isTrichotomous_lex

added theorem Pi.le_toLex_update_self_iff

added theorem Pi.lex_desc

added theorem Pi.lex_lt_of_lt

added theorem Pi.lex_lt_of_lt_of_preorder

added theorem Pi.lt_toLex_update_self_iff

added theorem Pi.ofLex_apply

added theorem Pi.toLex_apply

added theorem Pi.toLex_monotone

added theorem Pi.toLex_strictMono

added theorem Pi.toLex_update_le_self_iff

added theorem Pi.toLex_update_lt_self_iff

Modified Mathlib/Order/Max.lean

Modified Mathlib/Order/Synonym.lean