Theorems · Definition · order theory
InitialSeg.toRelEmbedding
{α : Type u_4} → {β : Type u_5} → {r : α → α → Prop} → {s : β → β → Prop} → InitialSeg r s → r ↪r s- Defined in
- Mathlib.Order.InitialSeg
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RelEmbeddingstatement · cited by 281
- InitialSegstatement and proof · cited by 70
Cited by15
Results whose statement or proof uses this declaration.
- Cardinal.lift_injectiveproof · cited by 12
- InitialSeg.toOrderEmbeddingproof · cited by 8
- Ordinal.liftPrincipalSegproof · cited by 6
- InitialSeg.transproof · cited by 5
- PrincipalSeg.transInitialproof · cited by 3
- Ordinal.type_le_iff'proof · cited by 3
- InitialSeg.map_rel_iffproof · cited by 2
- InitialSeg.principalSumRelIsoproof · cited by 2
- InitialSeg.toPrincipalSegproof · cited by 2
- InitialSeg.mem_range_of_rel'statement · cited by 1
- CategoryTheory.Limits.hasColimitsOfShape_of_initialSegproof · cited by 1
- InitialSeg.accproof · cited by 1