Theorem Prod.Lex.toLex_le_toLex

Modification history

2025-01-22 11:38
Mathlib/Data/Prod/Lex.lean
feat: definition of `<` on `α ×ₗ β` in partial orders (#20067) …
Added Prod.Lex.toLex_le_toLexView on Github →