Mathlib v3 is deprecated. Go to Mathlib v4

Inductive sigma.le

Modification history

2021-12-03 08:57

src/data/sigma/order.lean

feat(data/sigma{lex,order}): Lexicographic and disjoint orders on a sigma type (#10552) …

Added sigma.le View on Github →