Documentation Verification Report

Shrink

📁 Source: Mathlib/Order/Shrink.lean

Statistics

Metric	Count
Definitions `instBotShrink`, `instLinearOrderShrink`, `instOrderBotShrink`, `instOrderTopShrink`, `instPartialOrderShrink`, `instPredOrderShrink`, `instPreorderShrink`, `instSuccOrderShrink`, `instTopShrink`, `orderIsoShrink`	10
Theorems `equivShrink_bot`, `equivShrink_le_equivShrink`, `equivShrink_lt_equivShrink`, `equivShrink_symm_bot`, `equivShrink_symm_top`, `equivShrink_top`, `instWellFoundedGTShrink`, `instWellFoundedLTShrink`, `orderIsoShrink_apply`, `orderIsoShrink_symm_apply`	10
Total	20

(root)

Definitions

Name	Category	Theorems
`instBotShrink` 📖	CompOp	2 math math: `equivShrink_symm_bot`, `equivShrink_bot`
`instLinearOrderShrink` 📖	CompOp	—
`instOrderBotShrink` 📖	CompOp	—
`instOrderTopShrink` 📖	CompOp	—
`instPartialOrderShrink` 📖	CompOp	—
`instPredOrderShrink` 📖	CompOp	—
`instPreorderShrink` 📖	CompOp	6 math math: `instWellFoundedLTShrink`, `equivShrink_lt_equivShrink`, `orderIsoShrink_apply`, `orderIsoShrink_symm_apply`, `equivShrink_le_equivShrink`, `instWellFoundedGTShrink`
`instSuccOrderShrink` 📖	CompOp	—
`instTopShrink` 📖	CompOp	2 math math: `equivShrink_top`, `equivShrink_symm_top`
`orderIsoShrink` 📖	CompOp	2 math math: `orderIsoShrink_apply`, `orderIsoShrink_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivShrink_bot` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Bot.bot` `instBotShrink`	—	—
`equivShrink_le_equivShrink` 📖	mathematical	—	`Shrink` `Preorder.toLE` `instPreorderShrink` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink`	—	`RelIso.map_rel_iff`
`equivShrink_lt_equivShrink` 📖	mathematical	—	`Shrink` `Preorder.toLT` `instPreorderShrink` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink`	—	`RelIso.map_rel_iff`
`equivShrink_symm_bot` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Bot.bot` `instBotShrink`	—	`Equiv.injective` `Equiv.apply_symm_apply`
`equivShrink_symm_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink` `Top.top` `instTopShrink`	—	`Equiv.injective` `Equiv.apply_symm_apply`
`equivShrink_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Top.top` `instTopShrink`	—	—
`instWellFoundedGTShrink` 📖	mathematical	—	`WellFoundedGT` `Shrink` `Preorder.toLT` `instPreorderShrink`	—	`RelEmbedding.isWellFounded`
`instWellFoundedLTShrink` 📖	mathematical	—	`WellFoundedLT` `Shrink` `Preorder.toLT` `instPreorderShrink`	—	`RelEmbedding.isWellFounded`
`orderIsoShrink_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Shrink` `Preorder.toLE` `instPreorderShrink` `instFunLikeOrderIso` `orderIsoShrink` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink`	—	—
`orderIsoShrink_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Shrink` `Preorder.toLE` `instPreorderShrink` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoShrink` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink`	—	—

---

← Back to Index