Documentation Verification Report

Order

📁 Source: Mathlib/Data/Sym/Sym2/Order.lean

Statistics

Metric	Count
Definitions `inf`, `sortEquiv`, `sup`	3
Theorems `inf_eq_inf_and_sup_eq_sup`, `inf_le_sup`, `inf_mk`, `sortEquiv_apply_coe`, `sortEquiv_symm_apply`, `sup_mk`	6
Total	9

Sym2

Definitions

Name	Category	Theorems
`inf` 📖	CompOp	4 math math: `sortEquiv_apply_coe`, `inf_eq_inf_and_sup_eq_sup`, `inf_le_sup`, `inf_mk`
`sortEquiv` 📖	CompOp	2 math math: `sortEquiv_apply_coe`, `sortEquiv_symm_apply`
`sup` 📖	CompOp	4 math math: `sortEquiv_apply_coe`, `inf_eq_inf_and_sup_eq_sup`, `inf_le_sup`, `sup_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf_eq_inf_and_sup_eq_sup` 📖	mathematical	—	`inf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sup` `Lattice.toSemilatticeSup`	—	`ind` `le_total` `inf_of_le_left` `sup_of_le_right` `le_antisymm` `inf_of_le_right` `sup_of_le_left`
`inf_le_sup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `inf` `sup` `Lattice.toSemilatticeSup`	—	`ind`
`inf_mk` 📖	mathematical	—	`inf` `SemilatticeInf.toMin`	—	—
`sortEquiv_apply_coe` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `Sym2` `EquivLike.toFunLike` `Equiv.instEquivLike` `sortEquiv` `inf` `sup` `Lattice.toSemilatticeSup`	—	—
`sortEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Sym2` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sortEquiv`	—	—
`sup_mk` 📖	mathematical	—	`sup` `SemilatticeSup.toMax`	—	—

---

← Back to Index