Lex
📁 Source: Mathlib/Data/List/Lex.lean
Statistics
| Metric | Count |
|---|---|
| 3 | |
| 16 | |
| Total | 19 |
Decidable.List.Lex
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
ne_iff 📖 | — | — | — | — | List.Lex.to_nenot_lt_of_ge |
List
Definitions
| Name | Category | Theorems |
|---|---|---|
LE' 📖 | CompOp | |
instLinearOrder 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
cons_le_cons 📖 | — | LE' | — | — | le_iff_lt_or_eq |
head!_le_of_lt 📖 | mathematical | Preorder.toLT | Preorder.toLE | — | head_le_of_ltcons_head!_tail |
head_le_of_lt 📖 | mathematical | Preorder.toLT | Preorder.toLE | — | le_rflLT.lt.le |
lex_cons_iff 📖 | — | — | — | — | irrefl_of |
lex_nil_or_eq_nil 📖 | — | — | — | — | — |
lex_singleton_iff 📖 | — | — | — | — | — |
lt_iff_lex_lt 📖 | — | — | — | — | lt.eq_1 |
List.Lex
Definitions
| Name | Category | Theorems |
|---|---|---|
decidableRel 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
append_left 📖 | — | — | — | — | — |
append_right 📖 | — | — | — | — | — |
asymm 📖 | — | — | — | — | — |
imp 📖 | — | — | — | — | — |
isOrderConnected 📖 | mathematical | — | IsOrderConnected | — | — |
ne_iff 📖 | — | — | — | — | Decidable.List.Lex.ne_iff |
to_ne 📖 | — | — | — | — | — |
trichotomous 📖 | — | — | — | — | — |
---