Documentation Verification Report

WithTop

📁 Source: Mathlib/Algebra/Order/Sub/WithTop.lean

Statistics

Metric	Count
Definitions `instSub`, `sub`	2
Theorems `coe_sub`, `instOrderedSub`, `map_sub`, `sub_eq_top_iff`, `sub_ne_top_iff`, `sub_top`, `top_sub_coe`	7
Total	9

WithTop

Definitions

Name	Category	Theorems
`instSub` 📖	CompOp	6 math math: `sub_eq_top_iff`, `instOrderedSub`, `map_sub`, `top_sub_coe`, `coe_sub`, `sub_top`
`sub` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_sub` 📖	mathematical	—	`some` `WithTop` `instSub`	—	—
`instOrderedSub` 📖	mathematical	—	`OrderedSub` `WithTop` `instLE` `add` `instSub` `OrderBot.toBot`	—	`sub_top` `add_top` `tsub_le_iff_right`
`map_sub` 📖	mathematical	`Bot.bot`	`map` `WithTop` `instSub`	—	`sub_top`
`sub_eq_top_iff` 📖	mathematical	—	`WithTop` `instSub` `Top.top` `top`	—	`sub_top`
`sub_ne_top_iff` 📖	mathematical	—	`Top.top` `WithTop` `top`	—	—
`sub_top` 📖	mathematical	—	`WithTop` `instSub` `Top.top` `top` `some` `Bot.bot`	—	—
`top_sub_coe` 📖	mathematical	—	`WithTop` `instSub` `Top.top` `top` `some`	—	—

---

← Back to Index