Documentation Verification Report

PImage

📁 Source: Mathlib/Data/Finset/PImage.lean

Statistics

Metric	Count
Definitions `pimage`, `toFinset`	2
Theorems `coe_pimage`, `mem_pimage`, `pimage_congr`, `pimage_empty`, `pimage_eq_image_filter`, `pimage_inter`, `pimage_mono`, `pimage_some`, `pimage_subset`, `pimage_union`, `coe_toFinset`, `mem_toFinset`, `toFinset_none`, `toFinset_some`	14
Total	16

Finset

Definitions

Name	Category	Theorems
`pimage` 📖	CompOp	10 math math: `pimage_eq_image_filter`, `pimage_congr`, `pimage_union`, `mem_pimage`, `pimage_inter`, `pimage_subset`, `pimage_some`, `coe_pimage`, `pimage_empty`, `pimage_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_pimage` 📖	mathematical	—	`SetLike.coe` `Finset` `instSetLike` `pimage` `PFun.image`	—	`Set.ext` `mem_pimage`
`mem_pimage` 📖	mathematical	—	`Finset` `instMembership` `pimage` `Part` `Part.instMembership`	—	—
`pimage_congr` 📖	mathematical	—	`pimage`	—	`ext`
`pimage_empty` 📖	mathematical	—	`pimage` `Finset` `instEmptyCollection`	—	`ext`
`pimage_eq_image_filter` 📖	mathematical	—	`pimage` `image` `Finset` `instMembership` `filter` `Part.Dom` `Part.get` `Set` `Set.instMembership` `Multiset` `Multiset.instMembership` `val` `mem_filter` `Subtype.coe_prop` `attach`	—	`ext` `mem_filter` `Subtype.coe_prop`
`pimage_inter` 📖	mathematical	—	`Finset` `instHasSubset` `pimage` `instInter`	—	`coe_pimage` `coe_inter`
`pimage_mono` 📖	mathematical	`Finset` `instHasSubset`	`pimage`	—	`pimage_subset` `mem_pimage`
`pimage_some` 📖	mathematical	—	`pimage` `Part.some` `image`	—	`ext`
`pimage_subset` 📖	mathematical	—	`Finset` `instHasSubset` `pimage` `instMembership`	—	`forall_swap`
`pimage_union` 📖	mathematical	—	`pimage` `Finset` `instUnion`	—	`coe_pimage` `coe_union`

Part

Definitions

Name	Category	Theorems
`toFinset` 📖	CompOp	4 math math: `toFinset_some`, `coe_toFinset`, `toFinset_none`, `mem_toFinset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toFinset` 📖	mathematical	—	`SetLike.coe` `Finset` `Finset.instSetLike` `toFinset` `setOf` `Part` `instMembership`	—	`Set.ext` `mem_toFinset`
`mem_toFinset` 📖	mathematical	—	`Finset` `Finset.instMembership` `toFinset` `Part` `instMembership`	—	—
`toFinset_none` 📖	mathematical	—	`toFinset` `none` `Finset` `Finset.instEmptyCollection`	—	`none_toOption`
`toFinset_some` 📖	mathematical	—	`toFinset` `some` `Finset` `Finset.instSingleton`	—	`some_toOption`

---

← Back to Index