Mathlib Map

Theorems · Inductive type

Bot

Type u_1 → Type u_1

Typeclass for the ⊥ (\bot) notation

Defined in
Mathlib.Order.Notation
Cited by
96 results in Mathlib
Foundations
Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Bot.bot · cited by 4720Bot.botSupBotHom · cited by 54SupBotHomBotHom · cited by 37BotHomSupBotHom.comp · cited by 12SupBotHom.compBotHom.comp · cited by 12BotHom.compBotHomClass.map_bot · cited by 12BotHomClass.map_botSupBotHom.id · cited by 10SupBotHom.idBotHom.id · cited by 8BotHom.idBotHomClass · cited by 5BotHomClassSupBotHom.dual · cited by 5SupBotHom.dualBotHom.ext · cited by 5BotHom.extWithTop.sub_top · cited by 4WithTop.sub_topSupBotHomClass · cited by 4SupBotHomClassSupBotHom.ext · cited by 3SupBotHom.extSupBotHom.toSupHom · cited by 3SupBotHom.toSupHomBotCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by184

Results whose statement or proof uses this declaration.