Documentation Verification Report

Tuple

📁 Source: Mathlib/Order/Fin/Tuple.lean

Statistics

Metric	Count
Definitions `castLEOrderIso`, `consOrderIso`, `insertNthOrderIso`, `snocOrderIso`, `finTwoArrowIso`, `piFinTwoIso`, `finSuccAboveOrderIso`	7
Theorems `vecCons`, `castLEOrderIso_apply`, `castLEOrderIso_symm_apply`, `consOrderIso_apply`, `consOrderIso_symm_apply`, `consOrderIso_toEquiv`, `insertNthOrderIso_apply`, `insertNthOrderIso_last`, `insertNthOrderIso_symm_apply`, `insertNthOrderIso_toEquiv`, `insertNthOrderIso_zero`, `insertNth_mem_Icc`, `pi_lex_lt_cons_cons`, `preimage_insertNth_Icc_of_mem`, `preimage_insertNth_Icc_of_notMem`, `snocOrderIso_apply`, `snocOrderIso_symm_apply`, `snocOrderIso_toEquiv`, `vecCons`, `vecCons`, `vecCons`, `antitone_vecCons`, `antitone_vecEmpty`, `finSuccAboveOrderIso_apply`, `finSuccAboveOrderIso_symm_apply_last`, `finSuccAboveOrderIso_symm_apply_ne_last`, `liftFun_vecCons`, `monotone_vecCons`, `monotone_vecEmpty`, `strictAnti_vecCons`, `strictAnti_vecEmpty`, `strictMono_vecCons`, `strictMono_vecEmpty`	33
Total	40

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vecCons` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Preorder.toLE`	`Matrix.vecCons`	—	`antitone_vecCons`

Fin

Definitions

Name	Category	Theorems
`castLEOrderIso` 📖	CompOp	2 math math: `castLEOrderIso_symm_apply`, `castLEOrderIso_apply`
`consOrderIso` 📖	CompOp	4 math math: `consOrderIso_apply`, `consOrderIso_symm_apply`, `insertNthOrderIso_zero`, `consOrderIso_toEquiv`
`insertNthOrderIso` 📖	CompOp	5 math math: `insertNthOrderIso_symm_apply`, `insertNthOrderIso_toEquiv`, `insertNthOrderIso_zero`, `insertNthOrderIso_apply`, `insertNthOrderIso_last`
`snocOrderIso` 📖	CompOp	4 math math: `snocOrderIso_apply`, `snocOrderIso_symm_apply`, `snocOrderIso_toEquiv`, `insertNthOrderIso_last`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castLEOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `castLEOrderIso`	—	—
`castLEOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `RelIso.symm` `castLEOrderIso`	—	—
`consOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Prod.instLE_mathlib` `Pi.hasLe` `RelIso.instFunLike` `consOrderIso` `cons`	—	—
`consOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Pi.hasLe` `Prod.instLE_mathlib` `RelIso.instFunLike` `RelIso.symm` `consOrderIso` `tail`	—	—
`consOrderIso_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `Prod.instLE_mathlib` `Pi.hasLe` `consOrderIso` `consEquiv`	—	—
`insertNthOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Prod.instLE_mathlib` `Pi.hasLe` `succAbove` `RelIso.instFunLike` `insertNthOrderIso` `insertNth`	—	—
`insertNthOrderIso_last` 📖	mathematical	—	`insertNthOrderIso` `snocOrderIso`	—	`OrderIso.ext` `insertNth_last'`
`insertNthOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Pi.hasLe` `Prod.instLE_mathlib` `succAbove` `RelIso.instFunLike` `RelIso.symm` `insertNthOrderIso` `removeNth`	—	—
`insertNthOrderIso_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `Prod.instLE_mathlib` `Pi.hasLe` `succAbove` `insertNthOrderIso` `insertNthEquiv`	—	—
`insertNthOrderIso_zero` 📖	mathematical	—	`insertNthOrderIso` `consOrderIso`	—	`OrderIso.ext` `insertNthEquiv_zero`
`insertNth_mem_Icc` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Icc` `Pi.preorder` `insertNth` `succAbove`	—	—
`pi_lex_lt_cons_cons` 📖	mathematical	—	`Pi.Lex` `cons`	—	`cons_succ` `cons_zero` `instIsEmptyFalse`
`preimage_insertNth_Icc_of_mem` 📖	mathematical	`Set` `Set.instMembership` `Set.Icc`	`Set.preimage` `insertNth` `Pi.preorder` `succAbove`	—	`Set.ext`
`preimage_insertNth_Icc_of_notMem` 📖	mathematical	`Set` `Set.instMembership` `Set.Icc`	`Set.preimage` `insertNth` `Pi.preorder` `Set.instEmptyCollection`	—	`Set.ext`
`snocOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Prod.instLE_mathlib` `Pi.hasLe` `RelIso.instFunLike` `snocOrderIso` `snoc`	—	—
`snocOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Pi.hasLe` `Prod.instLE_mathlib` `RelIso.instFunLike` `RelIso.symm` `snocOrderIso` `init`	—	—
`snocOrderIso_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `Prod.instLE_mathlib` `Pi.hasLe` `snocOrderIso` `snocEquiv`	—	—

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vecCons` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Preorder.toLE`	`Matrix.vecCons`	—	`monotone_vecCons`

OrderIso

Definitions

Name	Category	Theorems
`finTwoArrowIso` 📖	CompOp	—
`piFinTwoIso` 📖	CompOp	—

StrictAnti

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vecCons` 📖	mathematical	`StrictAnti` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Preorder.toLT`	`Matrix.vecCons`	—	`strictAnti_vecCons`

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vecCons` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Preorder.toLT`	`Matrix.vecCons`	—	`strictMono_vecCons`

(root)

Definitions

Name	Category	Theorems
`finSuccAboveOrderIso` 📖	CompOp	2 math math: `finSuccAboveOrderIso_symm_apply_last`, `finSuccAboveOrderIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_vecCons` 📖	mathematical	—	`Antitone` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Preorder.toLE`	—	`monotone_vecCons`
`antitone_vecEmpty` 📖	mathematical	—	`Antitone` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Matrix.vecEmpty`	—	`le_rfl`
`finSuccAboveOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `finSuccAboveOrderIso` `Fin.succAbove` `Fin.succAbove_ne`	—	—
`finSuccAboveOrderIso_symm_apply_last` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `OrderIso.symm` `finSuccAboveOrderIso`	—	`Equiv.optionSubtype_apply_symm_apply` `Fin.succAbove_last`
`finSuccAboveOrderIso_symm_apply_ne_last` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finSuccAboveEquiv` `Fin.predAbove`	—	`Equiv.optionSubtype_apply_symm_apply` `finSuccEquiv'_ne_last_apply`
`liftFun_vecCons` 📖	mathematical	—	`Relator.LiftFun` `Matrix.vecCons`	—	`Fin.liftFun_iff_succ` `Matrix.cons_val_succ`
`monotone_vecCons` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Preorder.toLE`	—	`liftFun_vecCons` `instIsTransLe`
`monotone_vecEmpty` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Matrix.vecEmpty`	—	`le_refl`
`strictAnti_vecCons` 📖	mathematical	—	`StrictAnti` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Preorder.toLT`	—	`liftFun_vecCons` `instIsTransGt`
`strictAnti_vecEmpty` 📖	mathematical	—	`StrictAnti` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Matrix.vecEmpty`	—	`irrefl` `instIrreflLt`
`strictMono_vecCons` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Preorder.toLT`	—	`liftFun_vecCons` `instIsTransLt`
`strictMono_vecEmpty` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Matrix.vecCons` `Matrix.vecEmpty`	—	`irrefl` `instIrreflLt`

---

← Back to Index