Commit 2022-05-16 13:42 4586a97a

View on Github →

refactor(data/pi/lex): Use lex, provide notation (#14164) Delete pilex ι β in favor of lex (Π i, β i) which we provide Πₗ i, β i notation for.

Estimated changes

Modified src/combinatorics/colex.lean

Modified src/data/list/lex.lean

Modified src/data/pi/lex.lean

added theorem pi.lex.le_of_forall_le

deleted def pi.lex

added theorem pi.of_lex_apply

added theorem pi.to_lex_apply

deleted theorem pilex.le_of_forall_le

deleted def pilex

Modified src/data/prod/lex.lean

Modified src/data/psigma/order.lean

Modified src/data/sigma/order.lean