Documentation Verification Report

ULiftable

📁 Source: Mathlib/Control/ULiftable.lean

Statistics

Metric	Count
Definitions `instULiftableULiftULift`, `uliftable'`, `instULiftable`, `instULiftable`, `instULiftableULiftULift`, `uliftable'`, `instULiftableULiftULift`, `uliftable'`, `ULiftable`, `adaptDown`, `adaptUp`, `down`, `down'`, `downMap`, `refl`, `up`, `up'`, `upMap`, `instULiftableULiftULift`, `uliftable'`, `instULiftableContTULift`, `instULiftableId`, `instULiftableReaderTULift`, `instULiftableStateTULift`, `instULiftableWriterTULift`	25
Theorems `down_up`, `up_down`	2
Total	27

ContT

Definitions

Name	Category	Theorems
`instULiftableULiftULift` 📖	CompOp	—
`uliftable'` 📖	CompOp	—

Except

Definitions

Name	Category	Theorems
`instULiftable` 📖	CompOp	—

Option

Definitions

Name	Category	Theorems
`instULiftable` 📖	CompOp	—

ReaderT

Definitions

Name	Category	Theorems
`instULiftableULiftULift` 📖	CompOp	—
`uliftable'` 📖	CompOp	—

StateT

Definitions

Name	Category	Theorems
`instULiftableULiftULift` 📖	CompOp	—
`uliftable'` 📖	CompOp	—

ULiftable

Definitions

Name	Category	Theorems
`adaptDown` 📖	CompOp	—
`adaptUp` 📖	CompOp	—
`down` 📖	CompOp	2 math math: `up_down`, `down_up`
`down'` 📖	CompOp	—
`downMap` 📖	CompOp	—
`refl` 📖	CompOp	—
`up` 📖	CompOp	2 math math: `up_down`, `down_up`
`up'` 📖	CompOp	—
`upMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_up` 📖	mathematical	—	`down` `up`	—	`Equiv.left_inv`
`up_down` 📖	mathematical	—	`up` `down`	—	`Equiv.right_inv`

WriterT

Definitions

Name	Category	Theorems
`instULiftableULiftULift` 📖	CompOp	—
`uliftable'` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`ULiftable` 📖	CompData	—
`instULiftableContTULift` 📖	CompOp	—
`instULiftableId` 📖	CompOp	—
`instULiftableReaderTULift` 📖	CompOp	—
`instULiftableStateTULift` 📖	CompOp	—
`instULiftableWriterTULift` 📖	CompOp	—

---

← Back to Index