Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sigma.lex.mono

Modification history

2021-12-03 08:57
src/data/sigma/lex.lean
feat(data/sigma{lex,order}): Lexicographic and disjoint orders on a sigma type (#10552) …
Added sigma.lex.monoView on Github →