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.

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.

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 RelEmbedding : 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
• init' : ∀ (a : α) (b : β), s b (self.toRelEmbedding a) → ∃ (a' : α), self.toRelEmbedding a' = b

  The order embedding is an initial segment

theorem InitialSeg.init' {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} (self : r ≼i s) (a : α) (b : β) : s b (self.toRelEmbedding a) → ∃ (a' : α), self.toRelEmbedding a' = b

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))

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

• ⋯ = ⋯

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

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.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

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

An order isomorphism is an initial segment

Equations

• InitialSeg.ofIso f = { toRelEmbedding := f.toRelEmbedding, init' := ⋯ }

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

The identity function shows that ≼i is reflexive

Equations

• InitialSeg.refl r = { toRelEmbedding := RelEmbedding.refl r, init' := ⋯ }

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, init' := ⋯ }

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

theorem InitialSeg.Antisymm.aux {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] (f : r ≼i s) (g : s ≼i r) : Function.LeftInverse ⇑g ⇑f

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 : β), s x b ↔ ∃ (y : α), f y = x

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, init' := ⋯ }

@[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, init' := ⋯ }

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' := ⋯, init' := ⋯ }

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

• down' : ∀ (b : β), s b self.top ↔ ∃ (a : α), self.toRelEmbedding a = b

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

theorem PrincipalSeg.down' {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} (self : r ≺i s) (b : β) : s b self.top ↔ ∃ (a : α), self.toRelEmbedding a = b

The image 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))

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 }

@[simp]

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

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.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)) : ∃ (a' : α), f.toRelEmbedding a' = b

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, init' := ⋯ } }

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

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

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.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

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

Equations

• f.ltLe g = { toRelEmbedding := f.trans g.toRelEmbedding, top := g f.top, down' := ⋯ }

@[simp]

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)

@[simp]

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.ltLe { toRelEmbedding := g.toRelEmbedding, init' := ⋯ }

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

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

Equations

• PrincipalSeg.equivLT f g = { toRelEmbedding := f.toRelEmbedding.trans g.toRelEmbedding, top := g.top, down' := ⋯ }

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

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

Equations

• f.ltEquiv g = { toRelEmbedding := f.trans g.toRelEmbedding, top := g f.top, down' := ⋯ }

@[simp]

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)

@[simp]

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

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.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.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

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, down' := ⋯ }

@[simp]

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

@[simp]

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

@[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, ⋯⟩

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.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₂⟩, down' := ⋯ }

@[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 = let __src := RelEmbedding.ofIsEmpty r s; { toRelEmbedding := __src, top := b, down' := ⋯ }

@[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_wellFounded_subrel {β : Type u_4} {s : β → β → Prop} [IsTrans β s] : WellFounded s ↔ ∀ (b : β), WellFounded (Subrel s {b' : β | s b' b})

A relation is well-founded iff every principal segment of it is well-founded.

In this lemma we use Subrel to indicate its principal segments because it's usually more convenient to use.

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.ltOrEq {α : 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, hence one can take as top the minimum of the complement of the range) or an order isomorphism (if the range is everything).

Equations

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

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

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

noncomputable 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

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

Equations

• f.leLT g = match f.ltOrEq with | Sum.inl f' => f'.trans g | Sum.inr f' => PrincipalSeg.equivLT f' g

@[simp]

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.collapseF {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : r ↪r s) (a : α) : { b : β // ¬s (f a) b }

Given an order embedding into a well order, collapse the order embedding by filling the gaps, to obtain an initial segment. Here, we construct the collapsed order embedding pointwise, but the proof of the fact that it is an initial segment will be given in collapse.

Equations

• f.collapseF = ⋯.fix fun (a : α) (IH : (y : α) → r y a → { b : β // ¬s (f y) b }) => let S := {b : β | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩

theorem RelEmbedding.collapseF.lt {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : r ↪r s) {a : α} {a' : α} : r a' a → s ↑(f.collapseF a') ↑(f.collapseF a)

theorem RelEmbedding.collapseF.not_lt {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : r ↪r s) (a : α) {b : β} (h : ∀ (a' : α), r a' a → s (↑(f.collapseF a')) b) : ¬s b ↑(f.collapseF 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 from an order embedding into a well order, by collapsing it to fill the gaps.

Equations

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

theorem RelEmbedding.collapse_apply {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s] (f : r ↪r s) (a : α) : f.collapse a = ↑(f.collapseF a)