Mathlib Map

Theorems · Definition · order theory

RelHom.id

{α : Type u_1} → (r : α → α → Prop) → r →r r

Identity map is a relation homomorphism.

Defined in
Mathlib.Order.RelIso.Basic
Cited by
4 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SimpleGraph.Hom.id · cited by 11Hom.idRelHom.id_apply · cited by 3RelHom.id_applyRelHom.comp_id · cited by 0RelHom.comp_idRelHom.one_def · cited by 0RelHom.one_defRelHom.id_comp · cited by 0RelHom.id_compRelHom · cited by 49RelHomRelHom.idCITED BYCITES

Cites1

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

  • RelHomstatement · cited by 49

Cited by5

Results whose statement or proof uses this declaration.