Mathlib Map

Theorems · Definition · order theory

BotHom.id

(α : Type u_2) → [inst : Bot α] → BotHom α α

id as a BotHom.

Defined in
Mathlib.Order.Hom.Bounded
Cited by
8 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
Bot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BoundedOrderHom.id · cited by 8BoundedOrderHom.idHeytingHom.id · cited by 6HeytingHom.idTopHom.dual_id · cited by 0TopHom.dual_idBotHom.coe_id · cited by 0BotHom.coe_idBotHom.comp_id · cited by 0BotHom.comp_idBotHom.symm_dual_id · cited by 0BotHom.symm_dual_idBotHom.dual_id · cited by 0BotHom.dual_idBotHom.id_apply · cited by 0BotHom.id_applyBotHom.id_comp · cited by 0BotHom.id_compTopHom.symm_dual_id · cited by 0TopHom.symm_dual_idBot · cited by 96BotBotHom · cited by 37BotHomBotHom.idCITED BYCITES

Cites2

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

  • Botstatement and proof · cited by 96
  • BotHomstatement · cited by 37

Cited by10

Results whose statement or proof uses this declaration.