Documentation Verification Report

ToInt

📁 Source: Mathlib/Tactic/Order/ToInt.lean

Statistics

Metric	Count
Definitions `mkFinFun`, `toInt`, `translateToInt`	3
Theorems `exists_translation`, `toInt_eq_toInt`, `toInt_inf_toInt_eq_toInt`, `toInt_le_toInt`, `toInt_lt_toInt`, `toInt_ne_toInt`, `toInt_nle_toInt`, `toInt_nlt_toInt`, `toInt_sup_toInt_eq_toInt`	9
Total	12

Mathlib.Tactic.Order.ToInt

Definitions

Name	Category	Theorems
`mkFinFun` 📖	CompOp	—
`toInt` 📖	CompOp	7 math math: `toInt_sup_toInt_eq_toInt`, `toInt_le_toInt`, `toInt_nle_toInt`, `toInt_inf_toInt_eq_toInt`, `toInt_eq_toInt`, `toInt_nlt_toInt`, `toInt_lt_toInt`
`translateToInt` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_translation` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_trans` `le_total` `Mathlib.Tactic.Contrapose.contrapose₁` `lt_of_le_of_ne` `Mathlib.Tactic.Contrapose.contrapose₄`
`toInt_eq_toInt` 📖	mathematical	—	`toInt`	—	—
`toInt_inf_toInt_eq_toInt` 📖	mathematical	—	`toInt` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—
`toInt_le_toInt` 📖	mathematical	—	`toInt` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`exists_translation`
`toInt_lt_toInt` 📖	mathematical	—	`toInt` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Iff.not` `toInt_le_toInt`
`toInt_ne_toInt` 📖	—	—	—	—	`Iff.not` `toInt_eq_toInt`
`toInt_nle_toInt` 📖	mathematical	—	`toInt` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`toInt_lt_toInt`
`toInt_nlt_toInt` 📖	mathematical	—	`toInt` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`toInt_le_toInt`
`toInt_sup_toInt_eq_toInt` 📖	mathematical	—	`toInt` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—

---

← Back to Index