Initial and principal segments

This file defines initial and principal segments.

Main definitions

• InitialSeg r s: type of order embeddings of r into s for which the range is an initial segment (i.e., if b belongs to the range, then any b' < b also belongs to the range). It is denoted by r ≼i s.
• PrincipalSeg r s: Type of order embeddings of r into s for which the range is a principal segment, i.e., an interval of the form (-∞, top) for some element top. It is 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.

Notations

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 segments

Order embeddings whose range is an initial segment of s (i.e., if b belongs to the range, then any b' < b also belongs to the range). The type of these embeddings from r to s is called InitialSeg r s, and denoted by r ≼i s.

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 range is an initial segment. That is, whenever b < f a in β then b is in the range of f.

• toFun : α → β
• inj' : Function.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 «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 range is an initial segment. That is, whenever b < f a in β then b is in the range of f.

Equations

• «term_≼i_» = Lean.ParserDescr.trailingNode `«term_≼i_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼i ") (Lean.ParserDescr.cat `term 26))

def «term_≤i_» : Lean.TrailingParserDescr

An InitialSeg between the < relations of two types.

Equations

• «term_≤i_» = Lean.ParserDescr.trailingNode `«term_≤i_» 25 24 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤i ") (Lean.ParserDescr.cat `term 25))

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

Equations

• InitialSeg.instCoeRelEmbedding = { coe := InitialSeg.toRelEmbedding }

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

Equations

• InitialSeg.instFunLike = { coe := fun (f : r ≼i s) => f.toFun, coe_injective' := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• f.toOrderEmbedding = f.orderEmbeddingOfLTEmbedding

@[simp]

theorem InitialSeg.toOrderEmbedding_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) : ⇑f.toOrderEmbedding = ⇑f

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

Equations

• ⋯ = ⋯

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

@[simp]

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

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

@[deprecated InitialSeg.mem_range_of_rel]

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

Alias of InitialSeg.mem_range_of_rel.

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

theorem InitialSeg.inj {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i 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 : r ≼i s) {a : α} {b : β} : s b (f a) ↔ ∃ (a' : α), f a' = b ∧ r a' a

@[deprecated InitialSeg.exists_eq_iff_rel]

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

Alias of InitialSeg.exists_eq_iff_rel.

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

A relation isomorphism is an initial segment

Equations

• f.toInitialSeg = { toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := ⋯ }

@[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

@[deprecated RelIso.toInitialSeg]

def InitialSeg.ofIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) : r ≼i s

Alias of RelIso.toInitialSeg.

---

A relation isomorphism is an initial segment

Equations

• @InitialSeg.ofIso = @RelIso.toInitialSeg

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

The identity function shows that ≼i is reflexive

Equations

• InitialSeg.refl r = (RelIso.refl r).toInitialSeg

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

Equations

• InitialSeg.instInhabited r = { default := InitialSeg.refl r }

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

Composition of functions shows that ≼i is transitive

Equations

• f.trans g = { toRelEmbedding := f.trans g.toRelEmbedding, mem_range_of_rel' := ⋯ }

@[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 : r ≼i s) (g : s ≼i 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} [IsTrichotomous β s] [IsIrrefl β s] [IsWellFounded α r] : Subsingleton (r ≼i s)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

@[deprecated InitialSeg.eq_relIso]

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

Alias of InitialSeg.eq_relIso.

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

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

Equations

• f.antisymm g = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem InitialSeg.antisymm_toFun {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : r ≼i s) (g : s ≼i 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 : r ≼i s) (g : s ≼i 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 : r ≼i s) : Function.Surjective ⇑f ∨ ∃ (b : β), ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b

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

Restrict the codomain of an initial segment

Equations

• InitialSeg.codRestrict p f H = { toRelEmbedding := RelEmbedding.codRestrict p f.toRelEmbedding H, mem_range_of_rel' := ⋯ }

@[simp]

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

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

Initial segment from an empty type.

Equations

• InitialSeg.ofIsEmpty r s = { toRelEmbedding := RelEmbedding.ofIsEmpty r s, mem_range_of_rel' := ⋯ }

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

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

Equations

• InitialSeg.leAdd r s = { toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯, mem_range_of_rel' := ⋯ }

@[simp]

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

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

Principal segments

Order embeddings whose range is a principal segment of s (i.e., an interval of the form (-∞, top) for some element top of β). The type of these embeddings from r to s is called PrincipalSeg r s, and denoted by r ≺i s. Principal segments are in particular initial 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 order embedding whose range is an open interval (-∞, top) for some element top of β. Such order embeddings are called principal segments

• toFun : α → β
• inj' : Function.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 «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 range is an open interval (-∞, top) for some element top of β. Such order embeddings are called principal segments

Equations

• «term_≺i_» = Lean.ParserDescr.trailingNode `«term_≺i_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺i ") (Lean.ParserDescr.cat `term 26))

def «term_<i_» : Lean.TrailingParserDescr

A PrincipalSeg between the < relations of two types.

Equations

• «term_<i_» = Lean.ParserDescr.trailingNode `«term_<i_» 25 24 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <i ") (Lean.ParserDescr.cat `term 25))

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

Equations

• PrincipalSeg.instCoeOutRelEmbedding = { coe := PrincipalSeg.toRelEmbedding }

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

Equations

• PrincipalSeg.instCoeFunForall = { coe := fun (f : r ≺i s) => ⇑f.toRelEmbedding }

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

@[simp]

theorem PrincipalSeg.toRelEmbedding_inj {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsIrrefl β s] [IsTrichotomous β s] {f g : r ≺i s} : f.toRelEmbedding = g.toRelEmbedding ↔ f = g

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

@[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 : r ≺i s) {b : β} : b ∈ Set.range ⇑f.toRelEmbedding ↔ s b f.top

@[deprecated PrincipalSeg.mem_range_iff_rel]

theorem PrincipalSeg.down {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) {b : β} : s b f.top ↔ ∃ (a : α), f.toRelEmbedding a = b

theorem PrincipalSeg.lt_top {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i 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 : r ≺i 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 : r ≺i s) {a : α} {b : β} (h : s b (f.toRelEmbedding a)) : b ∈ Set.range ⇑f.toRelEmbedding

@[deprecated PrincipalSeg.mem_range_of_rel]

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

Alias of PrincipalSeg.mem_range_of_rel.

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

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

A principal segment is in particular an initial segment.

Equations

• PrincipalSeg.hasCoeInitialSeg = { coe := fun (f : r ≺i s) => { toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := ⋯ } }

theorem PrincipalSeg.coe_coe_fn' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : r ≺i 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 : r ≼i s) (g : r ≺i s) (a : α) : g.toRelEmbedding a = f a

@[deprecated InitialSeg.eq_principalSeg]

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

Alias of InitialSeg.eq_principalSeg.

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

@[deprecated PrincipalSeg.exists_eq_iff_rel]

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

Alias of PrincipalSeg.exists_eq_iff_rel.

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

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

Equations

• f.toPrincipalSeg hf = { toRelEmbedding := f.toRelEmbedding, top := Classical.choose ⋯, mem_range_iff_rel' := ⋯ }

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• f.transInitial g = { toRelEmbedding := f.trans g.toRelEmbedding, top := g f.top, mem_range_iff_rel' := ⋯ }

@[simp]

theorem PrincipalSeg.transInitial_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i s) (g : s ≼i 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 : r ≺i s) (g : s ≼i t) : (f.transInitial g).top = g f.top

@[deprecated PrincipalSeg.transInitial]

def PrincipalSeg.ltLe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i s) (g : s ≼i t) : r ≺i t

Alias of PrincipalSeg.transInitial.

---

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

Equations

• @PrincipalSeg.ltLe = @PrincipalSeg.transInitial

@[deprecated PrincipalSeg.transInitial_apply]

theorem PrincipalSeg.lt_le_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i s) (g : s ≼i t) (a : α) : (f.ltLe g).toRelEmbedding a = g (f.toRelEmbedding a)

@[deprecated PrincipalSeg.transInitial_top]

theorem PrincipalSeg.lt_le_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i s) (g : s ≼i t) : (f.ltLe 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 : r ≺i s) (g : s ≺i t) : r ≺i t

Composition of two principal segments as a principal segment.

Equations

• f.trans g = f.transInitial { toRelEmbedding := g.toRelEmbedding, mem_range_of_rel' := ⋯ }

@[simp]

theorem PrincipalSeg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsTrans γ t] (f : r ≺i s) (g : s ≺i 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 : r ≺i s) (g : s ≺i 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 : s ≺i t) : r ≺i t

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

Equations

• PrincipalSeg.relIsoTrans f g = { toRelEmbedding := f.toRelEmbedding.trans g.toRelEmbedding, top := g.top, mem_range_iff_rel' := ⋯ }

@[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 : s ≺i t) (a : α) : (PrincipalSeg.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 : s ≺i t) : (PrincipalSeg.relIsoTrans f g).top = g.top

@[deprecated PrincipalSeg.relIsoTrans]

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

Alias of PrincipalSeg.relIsoTrans.

---

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

Equations

• @PrincipalSeg.equivLT = @PrincipalSeg.relIsoTrans

@[deprecated PrincipalSeg.transInitial_top]

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

@[deprecated PrincipalSeg.transInitial_top]

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

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

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

Equations

• f.transRelIso g = f.transInitial g.toInitialSeg

@[deprecated PrincipalSeg.transRelIso]

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

Alias of PrincipalSeg.transRelIso.

---

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

Equations

• @PrincipalSeg.ltEquiv = @PrincipalSeg.transRelIso

@[simp]

theorem PrincipalSeg.transRelIso_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i 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 : r ≺i 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 (r ≺i s)

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

Equations

• ⋯ = ⋯

theorem PrincipalSeg.eq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f g : r ≺i 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 : r ≺i t) (g : s ≺i 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 : r ≺i s) (g : s ≺i t) (h : r ≺i t) : t h.top g.top

@[deprecated PrincipalSeg.top_rel_top]

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

Alias of PrincipalSeg.top_rel_top.

def PrincipalSeg.ofElement {α : Type u_4} (r : α → α → Prop) (a : α) : Subrel r {b : α | r b a} ≺i r

Any element of a well order yields a principal segment.

Equations

• PrincipalSeg.ofElement r a = { toRelEmbedding := Subrel.relEmbedding r {b : α | r b a}, top := a, mem_range_iff_rel' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def PrincipalSeg.subrelIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) : Subrel s {b : β | s b f.top} ≃r r

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

Equations

• f.subrelIso = { toEquiv := (Equiv.ofInjective ⇑f.toRelEmbedding ⋯).trans (Equiv.setCongr ⋯), map_rel_iff' := ⋯ }.symm

@[simp]

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

@[simp]

theorem PrincipalSeg.apply_subrelIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i 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 : r ≺i s) (a : α) : f.subrelIso ⟨f.toRelEmbedding a, ⋯⟩ = a

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

Restrict the codomain of a principal segment

Equations

• PrincipalSeg.codRestrict p f H H₂ = { toRelEmbedding := RelEmbedding.codRestrict p f.toRelEmbedding H, top := ⟨f.top, H₂⟩, mem_range_iff_rel' := ⋯ }

@[simp]

theorem PrincipalSeg.codRestrict_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : r ≺i s) (H : ∀ (a : α), f.toRelEmbedding a ∈ p) (H₂ : f.top ∈ p) (a : α) : (PrincipalSeg.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 : r ≺i s) (H : ∀ (a : α), f.toRelEmbedding a ∈ p) (H₂ : f.top ∈ p) : (PrincipalSeg.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) : r ≺i s

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

Equations

• PrincipalSeg.ofIsEmpty r H = { toRelEmbedding := RelEmbedding.ofIsEmpty r s, top := b, mem_range_iff_rel' := ⋯ }

@[simp]

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

@[reducible, inline]

abbrev PrincipalSeg.pemptyToPunit : EmptyRelation ≺i EmptyRelation

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

Equations

• PrincipalSeg.pemptyToPunit = PrincipalSeg.ofIsEmpty EmptyRelation ⋯

theorem PrincipalSeg.acc {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : r ≺i 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), r ≺i 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 : r ≼i s) : (r ≺i s) ⊕ (r ≃r s)

To an initial segment taking values in a well order, one can associate either a principal segment (if the range is not everything, taking the top the minimum of the complement of the range) or an order isomorphism (if the range is everything).

Equations

• f.principalSumRelIso = if h : Function.Surjective ⇑f then Sum.inr (RelIso.ofSurjective f.toRelEmbedding h) else Sum.inl (f.toPrincipalSeg h)

@[deprecated InitialSeg.principalSumRelIso]

def InitialSeg.ltOrEq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : r ≼i s) : (r ≺i s) ⊕ (r ≃r s)

Alias of InitialSeg.principalSumRelIso.

---

To an initial segment taking values in a well order, one can associate either a principal segment (if the range is not everything, taking the top the minimum of the complement of the range) or an order isomorphism (if the range is everything).

Equations

• @InitialSeg.ltOrEq = @InitialSeg.principalSumRelIso

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

Composition of an initial segment taking values in a well order and a principal segment.

Equations

• f.transPrincipal g = match f.principalSumRelIso with | Sum.inl f' => f'.trans g | Sum.inr f' => PrincipalSeg.relIsoTrans f' g

@[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 : r ≼i s) (g : s ≺i t) (a : α) : (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)

@[deprecated InitialSeg.transPrincipal]

def InitialSeg.leLT {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) : r ≺i t

Alias of InitialSeg.transPrincipal.

---

Composition of an initial segment taking values in a well order and a principal segment.

Equations

• @InitialSeg.leLT = @InitialSeg.transPrincipal

@[deprecated InitialSeg.transPrincipal_apply]

theorem InitialSeg.leLT_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) (a : α) : (f.leLT g).toRelEmbedding a = g.toRelEmbedding (f a)

noncomputable def RelEmbedding.collapse {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : r ↪r s) : r ≼i 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.

Equations

• f.collapse = { toRelEmbedding := RelEmbedding.ofMonotone (fun (a : α) => ↑(collapseF f a)) ⋯, mem_range_of_rel' := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

Initial or principal segments with <

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

An order isomorphism is an initial segment

Equations

• f.toInitialSeg = f.toRelIsoLT.toInitialSeg

@[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 : β} [Preorder α] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) (h : b ≤ f a) : b ∈ Set.range ⇑f

theorem InitialSeg.isLowerSet_range {α : Type u_1} {β : Type u_2} [PartialOrder β] [Preorder α] (f : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) : f a < f a' ↔ a < a'

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

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

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

@[simp]

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

theorem InitialSeg.le_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [LinearOrder α] (f : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : β} [LinearOrder α] (f : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : β} [Preorder α] (f : (fun (x1 x2 : α) => x1 < x2) ≺i 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 β] [Preorder α] (f : (fun (x1 x2 : α) => x1 < x2) ≺i 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 : (fun (x1 x2 : α) => x1 < x2) ≺i 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 : (fun (x1 x2 : α) => x1 < x2) ≺i 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 : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) : Monotone ⇑f.toRelEmbedding

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

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

@[simp]

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

theorem PrincipalSeg.le_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [LinearOrder α] (f : (fun (x1 x2 : α) => x1 < x2) ≺i 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 : β} [LinearOrder α] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) : b < f.toRelEmbedding a ↔ ∃ a' < a, f.toRelEmbedding a' = b