Initial and principal segments

This file defines initial and principal segment embeddings. Though these definitions make sense for arbitrary relations, they're intended for use with well orders.

An initial segment is simply a lower set, i.e. if x belongs to the range, then any y < x also belongs to the range. A principal segment is a set of the form Set.Iio x for some x.

An initial segment embedding r ≼i s is an order embedding r ↪ s such that its range is an initial segment. Likewise, a principal segment embedding r ≺i s has a principal segment for a range.

Main definitions

• InitialSeg r s: Type of initial segment embeddings of r into s, denoted by r ≼i s.
• PrincipalSeg r s: Type of principal segment embeddings of r into s, denoted by r ≺i s.

The lemmas Ordinal.type_le_iff and Ordinal.type_lt_iff tell us that ≼i corresponds to the ≤ relation on ordinals, while ≺i corresponds to the < relation. This prompts us to think of PrincipalSeg as a "strict" version of InitialSeg.

Notation

These notations belong to the InitialSeg locale.

• r ≼i s: the type of initial segment embeddings of r into s.
• r ≺i s: the type of principal segment embeddings of r into s.
• α ≤i β is an abbreviation for (· < ·) ≼i (· < ·).
• α <i β is an abbreviation for (· < ·) ≺i (· < ·).

Initial segment embeddings

structure InitialSeg {α : Type u_4} {β : Type u_5} (r : α → α → Prop) (s : β → β → Prop) extends r ↪r s : Type (max u_4 u_5)

If r is a relation on α and s in a relation on β, then f : r ≼i s is an order embedding whose Set.range is a lower set. That is, whenever b < f a in β then b is in the range of f.

• toFun : α → β
• inj' : Injective self.toFun
• map_rel_iff' {a b : α} : s (self.toEmbedding a) (self.toEmbedding b) ↔ r a b
• mem_range_of_rel' (a : α) (b : β) : s b (self.toRelEmbedding a) → b ∈ Set.range ⇑self.toRelEmbedding

  The order embedding is an initial segment

def InitialSeg.«term_≼i_» : Lean.TrailingParserDescr

If r is a relation on α and s in a relation on β, then f : r ≼i s is an order embedding whose Set.range is a lower set. That is, whenever b < f a in β then b is in the range of f.

def «term_≤i_» : Lean.TrailingParserDescr

An InitialSeg between the < relations of two types.

@[implicit_reducible]

instance InitialSeg.instCoeRelEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Coe (InitialSeg r s) (r ↪r s)

@[implicit_reducible]

instance InitialSeg.instFunLike {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : FunLike (InitialSeg r s) α β

instance InitialSeg.instEmbeddingLike {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : EmbeddingLike (InitialSeg r s) α β

instance InitialSeg.instRelHomClass {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : RelHomClass (InitialSeg r s) r s

def InitialSeg.toOrderEmbedding {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : α ↪o β

An initial segment embedding between the < relations of two partial orders is an order embedding.

@[simp]

theorem InitialSeg.toOrderEmbedding_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (x : α) : f.toOrderEmbedding x = f x

@[simp]

theorem InitialSeg.coe_toOrderEmbedding {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : ⇑f.toOrderEmbedding = ⇑f

instance InitialSeg.instOrderHomClassLt {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] : OrderHomClass (InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) α β

theorem InitialSeg.ext {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : InitialSeg r s} (h : ∀ (x : α), f x = g x) : f = g

theorem InitialSeg.ext_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : InitialSeg r s} : f = g ↔ ∀ (x : α), f x = g x

@[simp]

theorem InitialSeg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) : ⇑f.toRelEmbedding = ⇑f

theorem InitialSeg.mem_range_of_rel {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) {a : α} {b : β} : s b (f a) → b ∈ Set.range ⇑f

theorem InitialSeg.map_rel_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : InitialSeg r s) : s (f a) (f b) ↔ r a b

theorem InitialSeg.inj {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) {a b : α} : f a = f b ↔ a = b

theorem InitialSeg.exists_eq_iff_rel {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) {a : α} {b : β} : s b (f a) ↔ ∃ (a' : α), f a' = b ∧ r a' a

def RelIso.toInitialSeg {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) : InitialSeg r s

A relation isomorphism is an initial segment embedding

@[simp]

theorem RelIso.toInitialSeg_toFun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : α) : f.toInitialSeg a = f a

def InitialSeg.refl {α : Type u_1} (r : α → α → Prop) : InitialSeg r r

The identity function shows that ≼i is reflexive

@[implicit_reducible]

instance InitialSeg.instInhabited {α : Type u_1} (r : α → α → Prop) : Inhabited (InitialSeg r r)

def InitialSeg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : InitialSeg r s) (g : InitialSeg s t) : InitialSeg r t

Composition of functions shows that ≼i is transitive

@[simp]

theorem InitialSeg.refl_apply {α : Type u_1} {r : α → α → Prop} (x : α) : (InitialSeg.refl r) x = x

@[simp]

theorem InitialSeg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : InitialSeg r s) (g : InitialSeg s t) (a : α) : (f.trans g) a = g (f a)

instance InitialSeg.subsingleton_of_trichotomous_of_irrefl {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous s] [Std.Irrefl s] [IsWellFounded α r] : Subsingleton (InitialSeg r s)

instance InitialSeg.instSubsingletonOfIsWellOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] : Subsingleton (InitialSeg r s)

Given a well order s, there is at most one initial segment embedding of r into s.

theorem InitialSeg.eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f g : InitialSeg r s) (a : α) : f a = g a

theorem InitialSeg.eq_relIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s) (g : r ≃r s) (a : α) : g a = f a

def InitialSeg.antisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s) (g : InitialSeg s r) : r ≃r s

If we have order embeddings between α and β whose ranges are initial segments, and β is a well order, then α and β are order-isomorphic.

@[simp]

theorem InitialSeg.antisymm_toFun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s) (g : InitialSeg s r) : ⇑(f.antisymm g) = ⇑f

@[simp]

theorem InitialSeg.antisymm_symm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : InitialSeg r s) (g : InitialSeg s r) : (f.antisymm g).symm = g.antisymm f

theorem InitialSeg.eq_or_principal {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s) : Function.Surjective ⇑f ∨ ∃ (b : β), ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b

An initial segment embedding is either an isomorphism, or a principal segment embedding.

See also InitialSeg.ltOrEq.

def InitialSeg.codRestrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : InitialSeg r s) (H : ∀ (a : α), f a ∈ p) : InitialSeg r (Subrel s fun (x : β) => x ∈ p)

Restrict the codomain of an initial segment

@[simp]

theorem InitialSeg.codRestrict_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : InitialSeg r s) (H : ∀ (a : α), f a ∈ p) (a : α) : (codRestrict p f H) a = ⟨f a, ⋯⟩

def InitialSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] : InitialSeg r s

Initial segment embedding from an empty type.

def InitialSeg.leAdd {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) : InitialSeg r (Sum.Lex r s)

Initial segment embedding of an order r into the disjoint union of r and s.

@[simp]

theorem InitialSeg.leAdd_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (a : α) : (leAdd r s) a = Sum.inl a

theorem InitialSeg.acc {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) (a : α) : Acc r a ↔ Acc s (f a)

Principal segments

structure PrincipalSeg {α : Type u_4} {β : Type u_5} (r : α → α → Prop) (s : β → β → Prop) extends r ↪r s : Type (max u_4 u_5)

If r is a relation on α and s in a relation on β, then f : r ≺i s is an initial segment embedding whose range is Set.Iio x for some element x. If β is a well order, this is equivalent to the embedding not being surjective.

• toFun : α → β
• inj' : Injective self.toFun
• map_rel_iff' {a b : α} : s (self.toEmbedding a) (self.toEmbedding b) ↔ r a b
• top : β

  The supremum of the principal segment

• mem_range_iff_rel' (b : β) : b ∈ Set.range ⇑self.toRelEmbedding ↔ s b self.top

  The range of the order embedding is the set of elements b such that s b top

def InitialSeg.«term_≺i_» : Lean.TrailingParserDescr

If r is a relation on α and s in a relation on β, then f : r ≺i s is an initial segment embedding whose range is Set.Iio x for some element x. If β is a well order, this is equivalent to the embedding not being surjective.

def «term_<i_» : Lean.TrailingParserDescr

A PrincipalSeg between the < relations of two types.

@[implicit_reducible]

instance PrincipalSeg.instCoeOutRelEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : CoeOut (PrincipalSeg r s) (r ↪r s)

@[implicit_reducible]

instance PrincipalSeg.instCoeFunForall {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : CoeFun (PrincipalSeg r s) fun (x : PrincipalSeg r s) => α → β

theorem PrincipalSeg.toRelEmbedding_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl s] [Std.Trichotomous s] : Function.Injective toRelEmbedding

@[simp]

theorem PrincipalSeg.toRelEmbedding_inj {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl s] [Std.Trichotomous s] {f g : PrincipalSeg r s} : f.toRelEmbedding = g.toRelEmbedding ↔ f = g

theorem PrincipalSeg.ext {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl s] [Std.Trichotomous s] {f g : PrincipalSeg r s} (h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x) : f = g

theorem PrincipalSeg.ext_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Irrefl s] [Std.Trichotomous s] {f g : PrincipalSeg r s} : f = g ↔ ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x

@[simp]

theorem PrincipalSeg.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (t : β) (o : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b t) : ⇑{ toRelEmbedding := f, top := t, mem_range_iff_rel' := o }.toRelEmbedding = ⇑f

theorem PrincipalSeg.mem_range_iff_rel {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) {b : β} : b ∈ Set.range ⇑f.toRelEmbedding ↔ s b f.top

theorem PrincipalSeg.lt_top {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) (a : α) : s (f.toRelEmbedding a) f.top

theorem PrincipalSeg.mem_range_of_rel_top {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) {b : β} (h : s b f.top) : b ∈ Set.range ⇑f.toRelEmbedding

theorem PrincipalSeg.mem_range_of_rel {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : PrincipalSeg r s) {a : α} {b : β} (h : s b (f.toRelEmbedding a)) : b ∈ Set.range ⇑f.toRelEmbedding

theorem PrincipalSeg.surjOn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) : Set.SurjOn (⇑f.toRelEmbedding) Set.univ {b : β | s b f.top}

@[implicit_reducible]

instance PrincipalSeg.hasCoeInitialSeg {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] : Coe (PrincipalSeg r s) (InitialSeg r s)

A principal segment embedding is in particular an initial segment embedding.

theorem PrincipalSeg.coe_coe_fn' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : PrincipalSeg r s) : ⇑{ toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := ⋯ } = ⇑f.toRelEmbedding

theorem InitialSeg.eq_principalSeg {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s) (g : PrincipalSeg r s) (a : α) : g.toRelEmbedding a = f a

theorem PrincipalSeg.exists_eq_iff_rel {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : PrincipalSeg r s) {a : α} {b : β} : s b (f.toRelEmbedding a) ↔ ∃ (a' : α), f.toRelEmbedding a' = b ∧ r a' a

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

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

@[simp]

theorem InitialSeg.toPrincipalSeg_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s) (hf : ¬Function.Surjective ⇑f) (x : α) : (f.toPrincipalSeg hf).toRelEmbedding x = f x

theorem PrincipalSeg.irrefl {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] (f : PrincipalSeg r r) : False

instance PrincipalSeg.instIsEmptyOfIsWellOrder {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] : IsEmpty (PrincipalSeg r r)

def PrincipalSeg.transInitial {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : PrincipalSeg r s) (g : InitialSeg s t) : PrincipalSeg r t

Composition of a principal segment embedding with an initial segment embedding, as a principal segment embedding

@[simp]

theorem PrincipalSeg.transInitial_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : PrincipalSeg r s) (g : InitialSeg s t) (a : α) : (f.transInitial g).toRelEmbedding a = g (f.toRelEmbedding a)

@[simp]

theorem PrincipalSeg.transInitial_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : PrincipalSeg r s) (g : InitialSeg s t) : (f.transInitial g).top = g f.top

def PrincipalSeg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsTrans γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t) : PrincipalSeg r t

Composition of two principal segment embeddings as a principal segment embedding

@[simp]

theorem PrincipalSeg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsTrans γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t) (a : α) : (f.trans g).toRelEmbedding a = g.toRelEmbedding (f.toRelEmbedding a)

@[simp]

theorem PrincipalSeg.trans_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsTrans γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t) : (f.trans g).top = g.toRelEmbedding f.top

def PrincipalSeg.relIsoTrans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s) (g : PrincipalSeg s t) : PrincipalSeg r t

Composition of an order isomorphism with a principal segment embedding, as a principal segment embedding

@[simp]

theorem PrincipalSeg.relIsoTrans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s) (g : PrincipalSeg s t) (a : α) : (relIsoTrans f g).toRelEmbedding a = g.toRelEmbedding (f a)

@[simp]

theorem PrincipalSeg.relIsoTrans_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s) (g : PrincipalSeg s t) : (relIsoTrans f g).top = g.top

def PrincipalSeg.transRelIso {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : PrincipalSeg r s) (g : s ≃r t) : PrincipalSeg r t

Composition of a principal segment embedding with a relation isomorphism, as a principal segment embedding

@[simp]

theorem PrincipalSeg.transRelIso_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : PrincipalSeg r s) (g : s ≃r t) (a : α) : (f.transRelIso g).toRelEmbedding a = g (f.toRelEmbedding a)

@[simp]

theorem PrincipalSeg.transRelIso_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : PrincipalSeg r s) (g : s ≃r t) : (f.transRelIso g).top = g f.top

instance PrincipalSeg.instSubsingletonOfIsWellOrder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] : Subsingleton (PrincipalSeg r s)

Given a well order s, there is a most one principal segment embedding of r into s.

theorem PrincipalSeg.eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f g : PrincipalSeg r s) (a : α) : f.toRelEmbedding a = g.toRelEmbedding a

theorem PrincipalSeg.top_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder γ t] (e : r ≃r s) (f : PrincipalSeg r t) (g : PrincipalSeg s t) : f.top = g.top

theorem PrincipalSeg.top_rel_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t) (h : PrincipalSeg r t) : t h.top g.top

def PrincipalSeg.ofElement {α : Type u_4} (r : α → α → Prop) (a : α) : PrincipalSeg (Subrel r fun (x : α) => r x a) r

Any element of a well order yields a principal segment.

@[simp]

theorem PrincipalSeg.ofElement_toFun {α : Type u_4} (r : α → α → Prop) (a : α) (self : { x : α // r x a }) : (ofElement r a).toFun self = ↑self

@[simp]

theorem PrincipalSeg.ofElement_top {α : Type u_4} (r : α → α → Prop) (a : α) : (ofElement r a).top = a

@[simp]

theorem PrincipalSeg.ofElement_apply {α : Type u_4} (r : α → α → Prop) (a : α) (b : { x : α // r x a }) : (ofElement r a).toRelEmbedding b = ↑b

noncomputable def PrincipalSeg.subrelIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) : (Subrel s fun (x : β) => s x f.top) ≃r r

For any principal segment r ≺i s, there is a Subrel of s order isomorphic to r.

@[simp]

theorem PrincipalSeg.subrelIso_symm_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) (a✝ : α) : f.subrelIso.symm a✝ = (Equiv.subtypeEquivProp ⋯) ⟨f.toRelEmbedding a✝, ⋯⟩

@[simp]

theorem PrincipalSeg.apply_subrelIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) (b : { b : β // s b f.top }) : f.toRelEmbedding (f.subrelIso b) = ↑b

@[simp]

theorem PrincipalSeg.subrelIso_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) (a : α) : f.subrelIso ⟨f.toRelEmbedding a, ⋯⟩ = a

def PrincipalSeg.codRestrict {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : PrincipalSeg r s) (H : ∀ (a : α), f.toRelEmbedding a ∈ p) (H₂ : f.top ∈ p) : PrincipalSeg r (Subrel s fun (x : β) => x ∈ p)

Restrict the codomain of a principal segment embedding.

@[simp]

theorem PrincipalSeg.codRestrict_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : PrincipalSeg r s) (H : ∀ (a : α), f.toRelEmbedding a ∈ p) (H₂ : f.top ∈ p) (a : α) : (codRestrict p f H H₂).toRelEmbedding a = ⟨f.toRelEmbedding a, ⋯⟩

@[simp]

theorem PrincipalSeg.codRestrict_top {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : PrincipalSeg r s) (H : ∀ (a : α), f.toRelEmbedding a ∈ p) (H₂ : f.top ∈ p) : (codRestrict p f H H₂).top = ⟨f.top, H₂⟩

def PrincipalSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} {s : β → β → Prop} (r : α → α → Prop) [IsEmpty α] {b : β} (H : ∀ (b' : β), ¬s b' b) : PrincipalSeg r s

Principal segment from an empty type into a type with a minimal element.

@[simp]

theorem PrincipalSeg.ofIsEmpty_top {α : Type u_1} {β : Type u_2} {s : β → β → Prop} (r : α → α → Prop) [IsEmpty α] {b : β} (H : ∀ (b' : β), ¬s b' b) : (ofIsEmpty r H).top = b

@[reducible, inline]

abbrev PrincipalSeg.pemptyToPUnit : PrincipalSeg emptyRelation emptyRelation

Principal segment from the empty relation on PEmpty to the empty relation on PUnit.

@[deprecated PrincipalSeg.pemptyToPUnit (since := "2026-02-08")]

def PrincipalSeg.pemptyToPunit : PrincipalSeg emptyRelation emptyRelation

Alias of PrincipalSeg.pemptyToPUnit.

---

Principal segment from the empty relation on PEmpty to the empty relation on PUnit.

theorem PrincipalSeg.acc {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : PrincipalSeg r s) (a : α) : Acc r a ↔ Acc s (f.toRelEmbedding a)

theorem wellFounded_iff_principalSeg {β : Type u} {s : β → β → Prop} [IsTrans β s] : WellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop) (x : PrincipalSeg r s), WellFounded r

Properties of initial and principal segments

noncomputable def InitialSeg.principalSumRelIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s) : PrincipalSeg r s ⊕ (r ≃r s)

Every initial segment embedding into a well order can be turned into an isomorphism if surjective, or into a principal segment embedding if not.

noncomputable def InitialSeg.transPrincipal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder β s] [IsTrans γ t] (f : InitialSeg r s) (g : PrincipalSeg s t) : PrincipalSeg r t

Composition of an initial segment embedding and a principal segment embedding as a principal segment embedding

@[simp]

theorem InitialSeg.transPrincipal_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder β s] [IsTrans γ t] (f : InitialSeg r s) (g : PrincipalSeg s t) (a : α) : (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)

theorem InitialSeg.exists_sum_relIso {α : Type u_1} {r : α → α → Prop} {β : Type u} {s : β → β → Prop} [IsWellOrder β s] (f : InitialSeg r s) : ∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

An initial segment can be extended to an isomorphism by joining a second well order to the domain.

noncomputable def RelEmbedding.collapse {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : r ↪r s) : InitialSeg r s

Construct an initial segment embedding r ≼i s by "filling in the gaps". That is, each subsequent element in α is mapped to the least element in β that hasn't been used yet.

This construction is guaranteed to work as long as there exists some relation embedding r ↪r s.

noncomputable def InitialSeg.total {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] : InitialSeg r s ⊕ InitialSeg s r

For any two well orders, one is an initial segment of the other.

Initial or principal segments with <

def OrderIso.toInitialSeg {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2

An order isomorphism is an initial segment

@[simp]

theorem OrderIso.toInitialSeg_toFun {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) : f.toInitialSeg a = f a

theorem InitialSeg.mem_range_of_le {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [LT α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (h : b ≤ f a) : b ∈ Set.range ⇑f

theorem InitialSeg.isLowerSet_range {α : Type u_1} {β : Type u_2} [PartialOrder β] [LT α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : IsLowerSet (Set.range ⇑f)

@[simp]

theorem InitialSeg.le_iff_le {α : Type u_1} {β : Type u_2} [PartialOrder β] {a a' : α} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : f a ≤ f a' ↔ a ≤ a'

@[simp]

theorem InitialSeg.lt_iff_lt {α : Type u_1} {β : Type u_2} [PartialOrder β] {a a' : α} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : f a < f a' ↔ a < a'

theorem InitialSeg.monotone {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : Monotone ⇑f

theorem InitialSeg.strictMono {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : StrictMono ⇑f

@[simp]

theorem InitialSeg.isMin_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : IsMin (f a) ↔ IsMin a

theorem InitialSeg.map_isMin {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : IsMin a → IsMin (f a)

Alias of the reverse direction of InitialSeg.isMin_apply_iff.

@[simp]

theorem InitialSeg.map_bot {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] [OrderBot α] [OrderBot β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : f ⊥ = ⊥

theorem InitialSeg.image_Iio {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) : ⇑f '' Set.Iio a = Set.Iio (f a)

theorem InitialSeg.le_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : b ≤ f a ↔ ∃ c ≤ a, f c = b

theorem InitialSeg.lt_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : b < f a ↔ ∃ a' < a, f a' = b

theorem PrincipalSeg.mem_range_of_le {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [LT α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (h : b ≤ f.toRelEmbedding a) : b ∈ Set.range ⇑f.toRelEmbedding

theorem PrincipalSeg.isLowerSet_range {α : Type u_1} {β : Type u_2} [PartialOrder β] [LT α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : IsLowerSet (Set.range ⇑f.toRelEmbedding)

@[simp]

theorem PrincipalSeg.le_iff_le {α : Type u_1} {β : Type u_2} [PartialOrder β] {a a' : α} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : f.toRelEmbedding a ≤ f.toRelEmbedding a' ↔ a ≤ a'

@[simp]

theorem PrincipalSeg.lt_iff_lt {α : Type u_1} {β : Type u_2} [PartialOrder β] {a a' : α} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : f.toRelEmbedding a < f.toRelEmbedding a' ↔ a < a'

theorem PrincipalSeg.monotone {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : Monotone ⇑f.toRelEmbedding

theorem PrincipalSeg.strictMono {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : StrictMono ⇑f.toRelEmbedding

@[simp]

theorem PrincipalSeg.isMin_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : IsMin (f.toRelEmbedding a) ↔ IsMin a

theorem PrincipalSeg.map_isMin {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : IsMin a → IsMin (f.toRelEmbedding a)

Alias of the reverse direction of PrincipalSeg.isMin_apply_iff.

@[simp]

theorem PrincipalSeg.map_bot {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] [OrderBot α] [OrderBot β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : f.toRelEmbedding ⊥ = ⊥

theorem PrincipalSeg.image_Iio {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) : ⇑f.toRelEmbedding '' Set.Iio a = Set.Iio (f.toRelEmbedding a)

theorem PrincipalSeg.le_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : b ≤ f.toRelEmbedding a ↔ ∃ c ≤ a, f.toRelEmbedding c = b

theorem PrincipalSeg.lt_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : b < f.toRelEmbedding a ↔ ∃ a' < a, f.toRelEmbedding a' = b