WithBotTop

📁 Source: Mathlib/Order/WithBotTop.lean

Statistics

Metric	Count
Definitions EInt, WithBotTop, instCoe, rec	4
Theorems coe_injective, coe_le_coe, coe_lt_coe, coe_monotone, coe_ne_bot, coe_ne_top, coe_strictMono, rec_bot, rec_coe, rec_top, top_ne_bot	11
Total	15

WithBotTop

Definitions

Name	Category	Theorems
instCoe 📖	CompOp	—
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_injective 📖	mathematical	—	WithBotTop coe	—	—
coe_le_coe 📖	mathematical	—	WithBotTop WithBot.instLE WithTop WithTop.instLE coe	—	WithTop.coe_le_coe WithBot.coe_le_coe
coe_lt_coe 📖	mathematical	—	WithBotTop WithBot.instLT WithTop WithTop.instLT coe	—	WithTop.coe_lt_coe WithBot.coe_lt_coe
coe_monotone 📖	mathematical	—	Monotone WithBotTop WithBot.instPreorder WithTop WithTop.instPreorder coe	—	—
coe_ne_bot 📖	—	—	—	—	—
coe_ne_top 📖	—	—	—	—	—
coe_strictMono 📖	mathematical	—	StrictMono WithBotTop WithBot.instPreorder WithTop WithTop.instPreorder coe	—	StrictMono.comp WithBot.coe_strictMono WithTop.coe_strictMono
rec_bot 📖	mathematical	—	Bot.bot WithBotTop WithBot.bot WithTop	—	—
rec_coe 📖	mathematical	—	coe	—	—
rec_top 📖	mathematical	—	Top.top WithBotTop WithBot.instTop WithTop WithTop.top	—	—
top_ne_bot 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
EInt 📖	CompOp	—
WithBotTop 📖	CompOp	7 math math: WithBotTop.coe_strictMono, WithBotTop.rec_bot, WithBotTop.coe_le_coe, WithBotTop.coe_monotone, WithBotTop.rec_top, WithBotTop.coe_injective, WithBotTop.coe_lt_coe

---

← Back to Index