Theorem Prod.Lex.toLex_covBy_toLex_iff

Modification history

2025-04-24 16:21
Mathlib/Data/Prod/Lex.lean
feat(Prod/Lex): prove `Prod.Lex.covBy_iff` (#24185) …
Added Prod.Lex.toLex_covBy_toLex_iffView on Github →