Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sigma.lex_iff

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