Theorems · Definition · order theory
RelEmbedding.toRelHom
{α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → r →r sA relation embedding is also a relation homomorphism
- Defined in
- Mathlib.Order.RelIso.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RelEmbeddingstatement and proof · cited by 281
- RelHomstatement · cited by 49
- RelEmbedding.toEmbeddingproof · cited by 45
- Function.Embedding.toFunproof · cited by 25
Cited by20
Results whose statement or proof uses this declaration.
- SimpleGraph.Embedding.toHomproof · cited by 17
- SimpleGraph.Iso.connectedComponentEquivproof · cited by 5
- RelIso.relHomCongrproof · cited by 4
- SimpleGraph.Iso.mapEdgeSetproof · cited by 3
- wellFoundedGT_iff_monotone_chain_condition'proof · cited by 3
- SimpleGraph.IsAcyclic.embeddingproof · cited by 3
- SimpleGraph.IsCompleteMultipartite.colorable_of_cliqueFreeproof · cited by 2
- SimpleGraph.Embedding.mapEdgeSetproof · cited by 1
- SimpleGraph.Iso.connectedComponentEquiv_applystatement · cited by 0
- SimpleGraph.Iso.connectedComponentEquiv_symm_applystatement · cited by 0
- RelEmbedding.toOrderHom_injectivestatement and proof · cited by 0
- SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_compstatement · cited by 0