Documentation Verification Report

Quotient

📁 Source: Mathlib/Order/Quotient.lean

Statistics

Metric	Count
Definitions `instLE_mathlib`, `instLinearOrder`, `instPreorder`	3
Theorems `instIsTransLe`, `instReflLe_mathlib`, `instTotalLe_mathlib`, `le_def`, `lift_monotone`, `lt_of_mk_lt_mk`, `mk_le_mk`, `mk_lt_mk`, `mk_monotone`	9
Total	12

Quotient

Definitions

Name	Category	Theorems
`instLE_mathlib` 📖	CompOp	5 math math: `instIsTransLe`, `instReflLe_mathlib`, `le_def`, `instTotalLe_mathlib`, `mk_le_mk`
`instLinearOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	3 math math: `mk_monotone`, `lift_monotone`, `mk_lt_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTransLe` 📖	mathematical	—	`IsTrans` `instLE_mathlib`	—	—
`instReflLe_mathlib` 📖	mathematical	—	`instLE_mathlib`	—	`refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `instIsEquivEquiv`
`instTotalLe_mathlib` 📖	mathematical	—	`instLE_mathlib`	—	`total_of`
`le_def` 📖	mathematical	—	`instLE_mathlib`	—	—
`lift_monotone` 📖	mathematical	`Monotone`	`instPreorder` `Preorder.toLE`	—	`Eq.le` `LE.le.trans`
`lt_of_mk_lt_mk` 📖	—	`Set.OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.preimage` `Set` `Set.instSingletonSet` `Preorder.toLT` `instPreorder` `Preorder.toLE`	—	—	—
`mk_le_mk` 📖	mathematical	`Set.OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.preimage` `Set` `Set.instSingletonSet`	`instLE_mathlib` `Preorder.toLE`	—	`Relation.transGen_eq_self` `LE.le.trans` `not_le` `eq_iff_equiv` `Set.OrdConnected.out` `LT.lt.le` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `instIsEquivEquiv`
`mk_lt_mk` 📖	mathematical	`Set.OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.preimage` `Set` `Set.instSingletonSet`	`Preorder.toLT` `instPreorder` `Preorder.toLE`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_and_or_eq` `comm_of` `IsEquiv.toSymm` `instIsEquivEquiv`
`mk_monotone` 📖	mathematical	—	`Monotone` `instPreorder` `Preorder.toLE`	—	—

---

← Back to Index