Documentation Verification Report

Fintype

📁 Source: Mathlib/Logic/Equiv/Fintype.lean

Statistics

Metric	Count
Definitions `viaFintypeEmbedding`, `extendSubtype`, `toCompl`, `toEquivRange`	4
Theorems `viaFintypeEmbedding_apply_image`, `viaFintypeEmbedding_apply_mem_range`, `viaFintypeEmbedding_apply_notMem_range`, `extendSubtype_apply_of_mem`, `extendSubtype_apply_of_not_mem`, `extendSubtype_mem`, `extendSubtype_not_mem`, `toEquivRange_apply`, `toEquivRange_eq_ofInjective`, `toEquivRange_symm_apply_self`	10
Total	14

Equiv

Definitions

Name	Category	Theorems
`extendSubtype` 📖	CompOp	4 math math: `extendSubtype_mem`, `extendSubtype_not_mem`, `extendSubtype_apply_of_mem`, `extendSubtype_apply_of_not_mem`
`toCompl` 📖	CompOp	1 math math: `extendSubtype_apply_of_not_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extendSubtype_apply_of_mem` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `extendSubtype` `Equiv`	—	`sumCompl_symm_apply_of_pos` `sumCompl_apply_inl`
`extendSubtype_apply_of_not_mem` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `extendSubtype` `Equiv` `toCompl`	—	`sumCompl_symm_apply_of_neg` `sumCompl_apply_inr`
`extendSubtype_mem` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `extendSubtype`	—	`extendSubtype_apply_of_mem`
`extendSubtype_not_mem` 📖	mathematical	—	`DFunLike.coe` `Perm` `EquivLike.toFunLike` `instEquivLike` `extendSubtype`	—	`extendSubtype_apply_of_not_mem`

Equiv.Perm

Definitions

Name	Category	Theorems
`viaFintypeEmbedding` 📖	CompOp	4 math math: `viaFintypeEmbedding_sign`, `viaFintypeEmbedding_apply_image`, `viaFintypeEmbedding_apply_notMem_range`, `viaFintypeEmbedding_apply_mem_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`viaFintypeEmbedding_apply_image` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `viaFintypeEmbedding` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`viaFintypeEmbedding.eq_1` `extendDomain_apply_image`
`viaFintypeEmbedding_apply_mem_range` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `viaFintypeEmbedding` `Function.Embedding.invOfMemRange`	—	`Function.Embedding.injective` `extendDomain_apply_subtype`
`viaFintypeEmbedding_apply_notMem_range` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `viaFintypeEmbedding`	—	`viaFintypeEmbedding.eq_1` `extendDomain_apply_not_subtype`

Function.Embedding

Definitions

Name	Category	Theorems
`toEquivRange` 📖	CompOp	5 math math: `Fin.cycleIcc_to_cycleRange`, `toEquivRange_eq_ofInjective`, `toEquivRange_symm_apply_self`, `Fin.cycleIcc_def_le`, `toEquivRange_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toEquivRange_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set.Elem` `Set.range` `Function.Embedding` `Function.instFunLikeEmbedding` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquivRange` `Set` `Set.instMembership` `Set.mem_range_self`	—	—
`toEquivRange_eq_ofInjective` 📖	mathematical	—	`toEquivRange` `Equiv.ofInjective` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `injective`	—	`Equiv.ext` `injective`
`toEquivRange_symm_apply_self` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set.Elem` `Set.range` `Function.Embedding` `Function.instFunLikeEmbedding` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toEquivRange` `Set` `Set.instMembership` `Set.mem_range_self`	—	`Set.mem_range_self`

---

← Back to Index