Documentation Verification Report

IsDirectLimit

📁 Source: FLT/Mathlib/Algebra/IsDirectLimit.lean

Statistics

Metric	Count
Definitions `IsDirectLimit`, `lift`, `linearEquiv`, `lift`, `preimage`, `preimage_index`	6
Theorems `Equiv_apply`, `compatibility_module`, `instDirectLimitCoeLinearMapIdOfOfNonempty`, `lift_of`, `lift_unique`, `linearEquiv_apply`, `linearEquiv_symm_apply`, `compatibility`, `compatibility'`, `image_preimage`, `inj`, `is_injective`, `is_surjective`, `lift_of`, `linearEquiv_symm_apply`, `surj`, `isDirectLimit_iff`	17
Total	23

IsDirectLimit

Definitions

Name	Category	Theorems
`lift` 📖	CompOp	1 math math: `lift_of`
`preimage` 📖	CompOp	1 math math: `image_preimage`
`preimage_index` 📖	CompOp	1 math math: `image_preimage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Equiv_apply` 📖	mathematical	—	`Equiv`	—	`lift_of` `compatibility'`
`compatibility` 📖	—	—	—	—	—
`compatibility'` 📖	—	—	—	—	`compatibility`
`image_preimage` 📖	mathematical	—	`preimage_index` `preimage`	—	`is_surjective`
`inj` 📖	—	—	—	—	—
`is_injective` 📖	—	—	—	—	—
`is_surjective` 📖	—	—	—	—	`surj`
`lift_of` 📖	mathematical	—	`lift`	—	`is_injective` `image_preimage`
`linearEquiv_symm_apply` 📖	mathematical	—	`Equiv`	—	`lift_of` `compatibility'`
`surj` 📖	—	—	—	—	—

IsDirectLimit.Module

Definitions

Name	Category	Theorems
`lift` 📖	CompOp	2 math math: `lift_unique`, `lift_of`
`linearEquiv` 📖	CompOp	2 math math: `linearEquiv_apply`, `linearEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatibility_module` 📖	—	—	—	—	`IsDirectLimit.compatibility'`
`instDirectLimitCoeLinearMapIdOfOfNonempty` 📖	mathematical	—	`IsDirectLimit`	—	—
`lift_of` 📖	mathematical	—	`lift`	—	`IsDirectLimit.lift_of`
`lift_unique` 📖	mathematical	—	`lift` `IsDirectLimit.compatibility`	—	`IsDirectLimit.compatibility` `IsDirectLimit.image_preimage`
`linearEquiv_apply` 📖	mathematical	—	`linearEquiv`	—	`IsDirectLimit.Equiv_apply`
`linearEquiv_symm_apply` 📖	mathematical	—	`linearEquiv`	—	`IsDirectLimit.linearEquiv_symm_apply`

(root)

Definitions

Name	Category	Theorems
`IsDirectLimit` 📖	CompData	4 math math: `IsDirectLimit.Module.instDirectLimitCoeLinearMapIdOfOfNonempty`, `RestrictedProduct.instIsDirectLimit`, `isDirectLimit_iff`, `RestrictedProduct.instIsDirectLimit'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDirectLimit_iff` 📖	mathematical	—	`IsDirectLimit`	—	—

---

← Back to Index