Theorem Prod.Lex.monotone_fst_ofLex

Modification history

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