Mathlib Map

Theorems · Definition · order theory

TopHom.id

(α : Type u_2) → [inst : Top α] → TopHom α α

id as a TopHom.

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

Around this declaration

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

BoundedOrderHom.id · cited by 8BoundedOrderHom.idCoheytingHom.id · cited by 4CoheytingHom.idTopHom.dual_id · cited by 0TopHom.dual_idTopHom.id_apply · cited by 0TopHom.id_applyTopHom.id_comp · cited by 0TopHom.id_compBotHom.symm_dual_id · cited by 0BotHom.symm_dual_idBotHom.dual_id · cited by 0BotHom.dual_idTopHom.coe_id · cited by 0TopHom.coe_idTopHom.comp_id · cited by 0TopHom.comp_idTopHom.symm_dual_id · cited by 0TopHom.symm_dual_idTop · cited by 93TopTopHom · cited by 37TopHomTopHom.idCITED BYCITES

Cites2

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

  • Topstatement and proof · cited by 93
  • TopHomstatement · cited by 37

Cited by10

Results whose statement or proof uses this declaration.