Theorems · Definition
Bot.bot
{α : Type u_1} → [self : Bot α] → αThe bot (⊥, \bot) element
Conventions for notations in identifiers:
* The recommended spelling of ⊥ in identifiers is bot.
- Defined in
- Mathlib.Order.Notation
- Cited by
- 4,720 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Bot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Botstatement and proof · cited by 96
Cited by5,170
Results whose statement or proof uses this declaration.
- Disjointproof · cited by 2,201
- LinearMap.kerproof · cited by 848
- Finset.supproof · cited by 530
- RingHom.kerproof · cited by 363
- bot_lestatement · cited by 306
- eq_bot_iffstatement · cited by 159
- IsAtomproof · cited by 130
- le_bot_iffstatement · cited by 116
- Ne.bot_ltstatement and proof · cited by 116
- WithBot.recBotCoestatement and proof · cited by 101
- bot_eq_zero'statement · cited by 92
- LinearMap.ker_eq_botstatement and proof · cited by 92
Showing the 200 most cited of 5,170.