Documentation Verification Report

NodupEquivFin

📁 Source: Mathlib/Data/List/NodupEquivFin.lean

Statistics

Metric	Count
Definitions `getBijectionOfForallMemList`, `getEquiv`, `getEquivOfForallMemList`, `getIso`, `getIso`, `getEquivOfForallCountEqOne`	6
Theorems `getBijectionOfForallMemList_coe`, `getEquivOfForallMemList_apply`, `getEquivOfForallMemList_symm_apply_val`, `getEquiv_apply_coe`, `getEquiv_symm_apply_val`, `coe_getIso_apply`, `coe_getIso_symm_apply`, `get_mono`, `get_strictMono`, `coe_getIso_apply`, `coe_getIso_symm_apply`, `duplicate_iff_exists_distinct_get`, `getEquivOfForallCountEqOne_apply`, `getEquivOfForallCountEqOne_symm_apply_val`, `sublist_iff_exists_fin_orderEmbedding_get_eq`, `sublist_iff_exists_orderEmbedding_getElem?_eq`, `sublist_of_orderEmbedding_getElem?_eq`	17
Total	23

List

Definitions

Name	Category	Theorems
`getEquivOfForallCountEqOne` 📖	CompOp	2 math math: `getEquivOfForallCountEqOne_apply`, `getEquivOfForallCountEqOne_symm_apply_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`duplicate_iff_exists_distinct_get` 📖	mathematical	—	`Duplicate`	—	`duplicate_iff_two_le_count` `sublist_iff_exists_fin_orderEmbedding_get_eq` `OrderEmbedding.lt_iff_lt` `instIsEmptyFalse` `OrderEmbedding.ofStrictMono.congr_simp`
`getEquivOfForallCountEqOne_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `getEquivOfForallCountEqOne`	—	—
`getEquivOfForallCountEqOne_symm_apply_val` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `getEquivOfForallCountEqOne`	—	—
`sublist_iff_exists_fin_orderEmbedding_get_eq` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`sublist_iff_exists_orderEmbedding_getElem?_eq` `Option.some_injective` `Fin.val_fin_lt` `OrderEmbedding.lt_iff_lt` `LT.lt.trans`
`sublist_iff_exists_orderEmbedding_getElem?_eq` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`OrderEmbedding.ofMapLEIff.congr_simp` `sublist_of_orderEmbedding_getElem?_eq`
`sublist_of_orderEmbedding_getElem?_eq` 📖	—	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	—	`OrderEmbedding.lt_iff_lt` `OrderEmbedding.le_iff_le` `OrderEmbedding.coe_ofMapLEIff`

List.Nodup

Definitions

Name	Category	Theorems
`getBijectionOfForallMemList` 📖	CompOp	1 math math: `getBijectionOfForallMemList_coe`
`getEquiv` 📖	CompOp	2 math math: `getEquiv_apply_coe`, `getEquiv_symm_apply_val`
`getEquivOfForallMemList` 📖	CompOp	2 math math: `getEquivOfForallMemList_apply`, `getEquivOfForallMemList_symm_apply_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`getBijectionOfForallMemList_coe` 📖	mathematical	—	`Function.Bijective` `getBijectionOfForallMemList`	—	—
`getEquivOfForallMemList_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `getEquivOfForallMemList`	—	—
`getEquivOfForallMemList_symm_apply_val` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `getEquivOfForallMemList`	—	—
`getEquiv_apply_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `getEquiv`	—	—
`getEquiv_symm_apply_val` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `getEquiv`	—	—

List.Sorted

Definitions

Name	Category	Theorems
`getIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_getIso_apply` 📖	mathematical	`List.SortedLT`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `List.SortedLT.getIso`	—	`List.SortedLT.coe_getIso_apply`
`coe_getIso_symm_apply` 📖	mathematical	`List.SortedLT`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `OrderIso.symm` `List.SortedLT.getIso`	—	`List.SortedLT.coe_getIso_symm_apply`
`get_mono` 📖	mathematical	`List.SortedLE`	`Monotone` `PartialOrder.toPreorder` `Fin.instPartialOrder`	—	`List.SortedLE.monotone_get`
`get_strictMono` 📖	mathematical	`List.SortedLT`	`StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder`	—	`List.SortedLT.strictMono_get`

List.SortedLT

Definitions

Name	Category	Theorems
`getIso` 📖	CompOp	4 math math: `coe_getIso_symm_apply`, `coe_getIso_apply`, `List.Sorted.coe_getIso_symm_apply`, `List.Sorted.coe_getIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_getIso_apply` 📖	mathematical	`List.SortedLT`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `getIso`	—	—
`coe_getIso_symm_apply` 📖	mathematical	`List.SortedLT`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `OrderIso.symm` `getIso`	—	—

---

← Back to Index