Bisect
📁 Source: Batteries/Data/Nat/Bisect.lean
Statistics
| Metric | Count |
|---|---|
| 2 | |
| 13 | |
| Total | 15 |
Nat
Definitions
| Name | Category | Theorems |
|---|---|---|
avg 📖 | CompOp | 7 mathmath:avg_le_right, le_avg_left, le_avg_right, avg_le_left, avg_lt_right, avg_comm, avg_lt_left |
bisect 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
avg_comm 📖 | mathematical | — | avg | — | avg.eq_1 |
avg_le_left 📖 | mathematical | — | avg | — | — |
avg_le_right 📖 | mathematical | — | avg | — | — |
avg_lt_left 📖 | mathematical | — | avg | — | — |
avg_lt_right 📖 | mathematical | — | avg | — | — |
bisect_add_one_false 📖 | mathematical | — | bisect | — | — |
bisect_lt_stop 📖 | mathematical | — | bisect | — | — |
bisect_true 📖 | mathematical | — | bisect | — | — |
le_add_one_of_avg_eq_left 📖 | — | avg | — | — | — |
le_add_one_of_avg_eq_right 📖 | — | avg | — | — | — |
le_avg_left 📖 | mathematical | — | avg | — | — |
le_avg_right 📖 | mathematical | — | avg | — | — |
start_le_bisect 📖 | mathematical | — | bisect | — | — |
---