Mathlib Map

Theorems · Definition · order theory

BotHom.comp

{α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} → [inst : Bot α] → [inst_1 : Bot β] → [inst_2 : Bot γ] → BotHom β γ → BotHom α β → BotHom α γ

Composition of BotHoms as a BotHom.

Defined in
Mathlib.Order.Hom.Bounded
Cited by
12 results in Mathlib
Foundations
Depth 9 from the axioms · uses no axioms
Assumes
BotBotBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BoundedOrderHom.comp · cited by 14BoundedOrderHom.compSupBotHom.comp · cited by 12SupBotHom.compBotHom.comp_apply · cited by 1BotHom.comp_applyBotHom.cancel_right · cited by 0BotHom.cancel_rightTopHom.dual_comp · cited by 0TopHom.dual_compBotHom.coe_comp · cited by 0BotHom.coe_compBotHom.comp_assoc · cited by 0BotHom.comp_assocBotHom.comp_id · cited by 0BotHom.comp_idBotHom.symm_dual_comp · cited by 0BotHom.symm_dual_compBotHom.dual_comp · cited by 0BotHom.dual_compBotHom.id_comp · cited by 0BotHom.id_compBoundedOrderHom.coe_comp_botHom · cited by 0BoundedOrderHom.coe_comp_…TopHom.symm_dual_comp · cited by 0TopHom.symm_dual_compBotHom.cancel_left · cited by 0BotHom.cancel_leftDFunLike.coe · cited by 62936DFunLike.coeBot · cited by 96BotBotHom · cited by 37BotHomBotHom.compCITED BYCITES

Cites3

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

  • DFunLike.coeproof · cited by 62,936
  • Botstatement and proof · cited by 96
  • BotHomstatement and proof · cited by 37

Cited by14

Results whose statement or proof uses this declaration.