Mathlib Map

Theorems · Definition · order theory

BotHom.toFun

{α : Type u_6} → {β : Type u_7} → [inst : Bot α] → [inst_1 : Bot β] → BotHom α β → α → β

The underlying function. The preferred spelling is DFunLike.coe.

Defined in
Mathlib.Order.Hom.Bounded
Cited by
1 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
BotBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BotHom.map_bot' · cited by 0BotHom.map_bot'Bot · cited by 96BotBotHom · cited by 37BotHomBotHom.toFunCITED 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 and proof · cited by 37

Cited by1

Results whose statement or proof uses this declaration.