Documentation Verification Report

IntervalCases

📁 Source: Mathlib/Tactic/IntervalCases.lean

Statistics

Metric	Count
Definitions `asLower`, `asUpper`, `IntervalCasesSubgoal`, `goal`, `rhs`, `value`, `Methods`, `bisect`, `eval`, `getBound`, `inconsistentBounds`, `initLB`, `initUB`, `mkNumeral`, `proveLE`, `proveLT`, `roundDown`, `roundUp`, `intMethods`, `intervalCases`, `natMethods`, `parseBound`, `intervalCases`	23
Theorems `add_one_le_of_not_le`, `le_sub_one_of_not_le`, `le_of_not_le_of_le`, `of_le_left`, `of_le_right`, `of_lt_left`, `of_lt_right`, `of_not_le_left`, `of_not_le_right`, `of_not_lt_left`, `of_not_lt_right`	11
Total	34

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_one_le_of_not_le` 📖	—	—	—	—	—
`le_sub_one_of_not_le` 📖	—	—	—	—	—

Mathlib.Tactic

Definitions

Name	Category	Theorems
`intervalCases` 📖	CompOp	—

Mathlib.Tactic.IntervalCases

Definitions

Name	Category	Theorems
`IntervalCasesSubgoal` 📖	CompData	—
`Methods` 📖	CompData	—
`intMethods` 📖	CompOp	—
`intervalCases` 📖	CompOp	—
`natMethods` 📖	CompOp	—
`parseBound` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_of_not_le_of_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`le_trans` `le_of_not_ge`
`of_le_left` 📖	—	—	—	—	—
`of_le_right` 📖	—	—	—	—	—
`of_lt_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`not_le`
`of_lt_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`not_le`
`of_not_le_left` 📖	—	—	—	—	—
`of_not_le_right` 📖	—	—	—	—	—
`of_not_lt_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`not_lt`
`of_not_lt_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`not_lt`

Mathlib.Tactic.IntervalCases.Bound

Definitions

Name	Category	Theorems
`asLower` 📖	CompOp	—
`asUpper` 📖	CompOp	—

Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal

Definitions

Name	Category	Theorems
`goal` 📖	CompOp	—
`rhs` 📖	CompOp	—
`value` 📖	CompOp	—

Mathlib.Tactic.IntervalCases.Methods

Definitions

Name	Category	Theorems
`bisect` 📖	CompOp	—
`eval` 📖	CompOp	—
`getBound` 📖	CompOp	—
`inconsistentBounds` 📖	CompOp	—
`initLB` 📖	CompOp	—
`initUB` 📖	CompOp	—
`mkNumeral` 📖	CompOp	—
`proveLE` 📖	CompOp	—
`proveLT` 📖	CompOp	—
`roundDown` 📖	CompOp	—
`roundUp` 📖	CompOp	—

---

← Back to Index