Bound

📁 Source: Mathlib/Tactic/Bound.lean

Statistics

Metric	Count
Definitions boundConfig, boundLinarith, boundNormNum, Bound, «tacticBound[_]»	5
Theorems cast_pos_of_pos, one_le_cast_of_le, le_max_of_le_left_or_le_right, lt_max_of_lt_left_or_lt_right, min_le_of_left_le_or_right_le, min_lt_of_left_lt_or_right_lt	6
Total	11

Mathlib.Tactic.Bound

Definitions

Name	Category	Theorems
boundConfig 📖	CompOp	—
boundLinarith 📖	CompOp	—
boundNormNum 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_max_of_le_left_or_le_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_max_iff
lt_max_of_lt_left_or_lt_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup	—	lt_max_iff
min_le_of_left_le_or_right_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeInf.toMin	—	min_le_iff
min_lt_of_left_lt_or_right_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeInf.toMin	—	min_lt_iff

Mathlib.Tactic.Bound.Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_pos_of_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Nat.cast_pos
one_le_cast_of_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne AddMonoidWithOne.toNatCast	—	Nat.one_le_cast

Mathlib.Tactic.IntervalCases

Definitions

Name	Category	Theorems
Bound 📖	CompData	—

(root)

Definitions

Name	Category	Theorems
«tacticBound[_]» 📖	CompOp	—

---

← Back to Index