Preimage

Statistics

Metric	Count
Definitions	0
Theorems `prod_preimage`, `prod_preimage'`, `prod_preimage_of_bij`, `sum_preimage`, `sum_preimage'`, `sum_preimage_of_bij`	6
Total	6

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_preimage` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`prod` `preimage`	—	`prod_preimage'` `prod_filter_of_ne` `Not.imp_symm`
`prod_preimage'` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`prod` `preimage` `filter` `Set` `Set.instMembership` `Set.range`	—	`prod_image` `coe_preimage` `image_preimage`
`prod_preimage_of_bij` 📖	mathematical	`Set.BijOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`prod` `preimage` `Set.BijOn.injOn`	—	`prod_preimage` `Set.BijOn.injOn` `Set.BijOn.subset_range`
`sum_preimage` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `preimage`	—	`sum_preimage'` `sum_filter_of_ne` `Not.imp_symm`
`sum_preimage'` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`sum` `preimage` `filter` `Set` `Set.instMembership` `Set.range`	—	`sum_image` `coe_preimage` `Set.mem_preimage` `SetLike.mem_coe` `image_preimage`
`sum_preimage_of_bij` 📖	mathematical	`Set.BijOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`sum` `preimage` `Set.BijOn.injOn`	—	`sum_preimage` `Set.BijOn.injOn` `Set.BijOn.subset_range`

---