Mathlib Map

Theorems · Definition · order theory

RelHom.toFun

{α : Type u_5} → {β : Type u_6} → {r : α → α → Prop} → {s : β → β → Prop} → r →r s → α → β

The underlying function of a RelHom

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

Around this declaration

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

RelSeries.map · cited by 6RelSeries.mapRelHom.map_rel' · cited by 4RelHom.map_rel'SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom · cited by 0SimpleGraph.nonempty_hom_…SimpleGraph.FinsubgraphHom.restrict · cited by 0FinsubgraphHom.restrictSimpleGraph.colorable_iff_exists_bdd_nat_coloring · cited by 0SimpleGraph.colorable_iff…RelHom.coe_fn_toFun · cited by 0RelHom.coe_fn_toFunRelHom · cited by 49RelHomRelHom.toFunCITED BYCITES

Cites1

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

  • RelHomstatement and proof · cited by 49

Cited by6

Results whose statement or proof uses this declaration.