Documentation Verification Report

ULift

📁 Source: Mathlib/Data/ULift.lean

Statistics

Metric	Count
Definitions `instDecidableEq_mathlib`, `instUnique`, `instDecidableEq_mathlib`, `instUnique`	4
Theorems `down_bijective`, `down_surjective`, `exists`, `forall`, `instIsEmpty`, `instNonempty_mathlib`, `map_bijective`, `map_injective`, `map_surjective`, `up_bijective`, `up_inj`, `up_injective`, `up_surjective`, `down_bijective`, `down_surjective`, `exists`, `ext`, `ext_iff`, `forall`, `instIsEmpty`, `instNonempty_mathlib`, `map_bijective`, `map_injective`, `map_surjective`, `rec_update`, `up_bijective`, `up_inj`, `up_injective`, `up_surjective`	29
Total	33

PLift

Definitions

Name	Category	Theorems
`instDecidableEq_mathlib` 📖	CompOp	—
`instUnique` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_bijective` 📖	mathematical	—	`Function.Bijective`	—	`Equiv.bijective`
`down_surjective` 📖	—	—	—	—	`Equiv.surjective`
`exists` 📖	—	—	—	—	`Function.Surjective.exists` `up_surjective`
`forall` 📖	—	—	—	—	`Function.Surjective.forall` `up_surjective`
`instIsEmpty` 📖	mathematical	—	`IsEmpty`	—	`Equiv.isEmpty`
`instNonempty_mathlib` 📖	—	—	—	—	`Equiv.nonempty`
`map_bijective` 📖	mathematical	—	`Function.Bijective` `map`	—	`Function.Bijective.of_comp_iff` `down_bijective` `Function.Bijective.of_comp_iff'` `up_bijective`
`map_injective` 📖	mathematical	—	`map`	—	`Function.Injective.of_comp_iff'` `down_bijective` `Function.Injective.of_comp_iff` `up_injective`
`map_surjective` 📖	mathematical	—	`map`	—	`Function.Surjective.of_comp_iff` `down_surjective` `Function.Surjective.of_comp_iff'` `up_bijective`
`up_bijective` 📖	mathematical	—	`Function.Bijective`	—	`Equiv.bijective`
`up_inj` 📖	—	—	—	—	—
`up_injective` 📖	—	—	—	—	`Equiv.injective`
`up_surjective` 📖	—	—	—	—	`Equiv.surjective`

ULift

Definitions

Name	Category	Theorems
`instDecidableEq_mathlib` 📖	CompOp	1 math math: `rec_update`
`instUnique` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_bijective` 📖	mathematical	—	`Function.Bijective`	—	`Equiv.bijective`
`down_surjective` 📖	—	—	—	—	`Equiv.surjective`
`exists` 📖	—	—	—	—	`Function.Surjective.exists` `up_surjective`
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`forall` 📖	—	—	—	—	`Function.Surjective.forall` `up_surjective`
`instIsEmpty` 📖	mathematical	—	`IsEmpty`	—	`Equiv.isEmpty`
`instNonempty_mathlib` 📖	—	—	—	—	`Equiv.nonempty`
`map_bijective` 📖	mathematical	—	`Function.Bijective` `map`	—	`Function.Bijective.of_comp_iff` `down_bijective` `Function.Bijective.of_comp_iff'` `up_bijective`
`map_injective` 📖	mathematical	—	`map`	—	`Function.Injective.of_comp_iff'` `down_bijective` `Function.Injective.of_comp_iff` `up_injective`
`map_surjective` 📖	mathematical	—	`map`	—	`Function.Surjective.of_comp_iff` `down_surjective` `Function.Surjective.of_comp_iff'` `up_bijective`
`rec_update` 📖	mathematical	—	`Function.update` `instDecidableEq_mathlib`	—	`Function.rec_update` `up_injective`
`up_bijective` 📖	mathematical	—	`Function.Bijective`	—	`Equiv.bijective`
`up_inj` 📖	—	—	—	—	—
`up_injective` 📖	—	—	—	—	`Equiv.injective`
`up_surjective` 📖	—	—	—	—	`Equiv.surjective`

---

← Back to Index