Theorems · Definition · order theory

InitialSeg.toPrincipalSeg

{α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} → [IsWellOrder β s] → (f : InitialSeg r s) → ¬Function.Surjective ⇑f → PrincipalSeg r s

A principal segment is the same as a non-surjective initial segment.

Defined in: Mathlib.Order.InitialSeg
Cited by: 2 results in Mathlib
Foundations: Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: IsWellOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

DFunLike.coestatement and proof · cited by 62,936
IsWellOrderstatement and proof · cited by 171
PrincipalSegstatement · cited by 73
InitialSegstatement and proof · cited by 70
InitialSeg.toRelEmbeddingproof · cited by 8

Cited by3

Results whose statement or proof uses this declaration.

InitialSeg.principalSumRelIsoproof · cited by 2
CategoryTheory.Limits.hasColimitsOfShape_of_initialSegproof · cited by 1
InitialSeg.toPrincipalSeg_applystatement · cited by 0