Documentation Verification Report

FiberPartition

📁 Source: Mathlib/Logic/Function/FiberPartition.lean

Statistics

Metric	Count
Definitions `image`, `mk`, `mkSelf`, `preimage`	4
Theorems `eq_fiber_image`, `fiber_nonempty`, `image_eq_image_mk`, `map_eq_image`, `map_preimage_eq_image`, `map_preimage_eq_image_map`, `mem_iff_eq_image`, `mk_image`	8
Total	12

Function.Fiber

Definitions

Name	Category	Theorems
`image` 📖	CompOp	7 math math: `map_eq_image`, `mem_iff_eq_image`, `map_preimage_eq_image_map`, `mk_image`, `eq_fiber_image`, `map_preimage_eq_image`, `image_eq_image_mk`
`mk` 📖	CompOp	—
`mkSelf` 📖	CompOp	—
`preimage` 📖	CompOp	4 math math: `map_preimage_eq_image_map`, `CompHausLike.LocallyConstant.incl_comap`, `map_preimage_eq_image`, `image_eq_image_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_fiber_image` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `Set.Elem` `Set.preimage` `Set.instSingletonSet` `image`	—	—
`fiber_nonempty` 📖	mathematical	—	`Set.Nonempty` `Set` `Set.instMembership` `Set.range` `Set.Elem` `Set.preimage` `Set.instSingletonSet`	—	`mem_iff_eq_image` `map_preimage_eq_image`
`image_eq_image_mk` 📖	mathematical	—	`image` `preimage`	—	`map_preimage_eq_image_map` `mk_image`
`map_eq_image` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `Set.Elem` `Set.preimage` `Set.instSingletonSet` `image`	—	`Set.mem_singleton_iff` `Set.mem_preimage` `Subtype.prop`
`map_preimage_eq_image` 📖	mathematical	—	`preimage` `image`	—	—
`map_preimage_eq_image_map` 📖	mathematical	—	`preimage` `image`	—	`map_preimage_eq_image`
`mem_iff_eq_image` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `Set.Elem` `Set.preimage` `Set.instSingletonSet` `image`	—	`map_eq_image` `eq_fiber_image`
`mk_image` 📖	mathematical	—	`image`	—	`map_eq_image`

---

← Back to Index