Documentation Verification Report

ULift

📁 Source: Mathlib/Control/ULift.lean

Statistics

Metric	Count
Definitions `bind`, `instMonad_mathlib`, `map`, `pure`, `seq`, `bind`, `instMonad_mathlib`, `map`, `pure`, `seq`	10
Theorems `bind_up`, `instLawfulApplicative_mathlib`, `instLawfulFunctor_mathlib`, `instLawfulMonad_mathlib`, `map_up`, `constant`, `seq_up`, `bind_up`, `instLawfulApplicative_mathlib`, `instLawfulFunctor_mathlib`, `instLawfulMonad_mathlib`, `map_up`, `constant`, `seq_up`	14
Total	24

PLift

Definitions

Name	Category	Theorems
`bind` 📖	CompOp	1 math math: `bind_up`
`instMonad_mathlib` 📖	CompOp	3 math math: `instLawfulMonad_mathlib`, `instLawfulApplicative_mathlib`, `instLawfulFunctor_mathlib`
`map` 📖	CompOp	4 math math: `map_up`, `map_surjective`, `map_bijective`, `map_injective`
`pure` 📖	CompOp	—
`seq` 📖	CompOp	1 math math: `seq_up`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_up` 📖	mathematical	—	`bind`	—	—
`instLawfulApplicative_mathlib` 📖	mathematical	—	`instMonad_mathlib`	—	`instLawfulFunctor_mathlib`
`instLawfulFunctor_mathlib` 📖	mathematical	—	`instMonad_mathlib`	—	—
`instLawfulMonad_mathlib` 📖	mathematical	—	`instMonad_mathlib`	—	`instLawfulApplicative_mathlib`
`map_up` 📖	mathematical	—	`map`	—	—
`seq_up` 📖	mathematical	—	`seq`	—	—

PLift.rec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constant` 📖	—	—	—	—	—

ULift

Definitions

Name	Category	Theorems
`bind` 📖	CompOp	1 math math: `bind_up`
`instMonad_mathlib` 📖	CompOp	3 math math: `instLawfulApplicative_mathlib`, `instLawfulMonad_mathlib`, `instLawfulFunctor_mathlib`
`map` 📖	CompOp	8 math math: `map_bijective`, `Topology.IsOpenEmbedding.uliftMap`, `Topology.IsClosedEmbedding.uliftMap`, `Topology.IsEmbedding.uliftMap`, `map_up`, `map_surjective`, `continuous_uliftMap`, `map_injective`
`pure` 📖	CompOp	—
`seq` 📖	CompOp	1 math math: `seq_up`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_up` 📖	mathematical	—	`bind`	—	—
`instLawfulApplicative_mathlib` 📖	mathematical	—	`instMonad_mathlib`	—	`instLawfulFunctor_mathlib`
`instLawfulFunctor_mathlib` 📖	mathematical	—	`instMonad_mathlib`	—	—
`instLawfulMonad_mathlib` 📖	mathematical	—	`instMonad_mathlib`	—	`instLawfulApplicative_mathlib`
`map_up` 📖	mathematical	—	`map`	—	—
`seq_up` 📖	mathematical	—	`seq`	—	—

ULift.rec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constant` 📖	—	—	—	—	—

---

← Back to Index