lex): Use `lex`, provide notation (#14164)

Commit

3 years ago

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

Author

YaelDillies

Parents

009669cb

mathlib 4586a97a - refactor(data/pi/lex): Use `lex`, provide notation (#14164)

mathlib
4586a97a - refactor(data/pi/lex): Use `lex`, provide notation (#14164)