Mathlib v3 is deprecated. Go to Mathlib v4

Inductive sigma.lex

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 View on Github →