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≼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)∞, top) for some element top. It is denoted by r ≺i s≺i s.

Notations

These notations belong to the InitialSeg locale.

• r ≼i s≼i s: the type of initial segment embeddings of r into s.
• r ≺i s≺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≼i s.

ink

structure InitialSeg {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) extends RelEmbedding : Type (maxu_1u_2)

• The order embedding is an initial segment

  init' : ∀ (a : α) (b : β), s b (↑toRelEmbedding.toEmbedding a) → ∃ a', ↑toRelEmbedding.toEmbedding a' = b

If r is a relation on α and s in a relation on β, then f : r ≼i s≼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.

ink

def «term_≼i_» : Lean.TrailingParserDescr

If r is a relation on α and s in a relation on β, then f : r ≼i s≼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))

ink

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

Equations

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

ink

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

Equations

• InitialSeg.instEmbeddingLikeInitialSeg = EmbeddingLike.mk (_ : ∀ (f : r ≼i s), Function.Injective f.toRelEmbedding.toEmbedding.toFun)

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

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

ink

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

The identity function shows that ≼i≼i is reflexive

Equations

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

ink

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

Equations

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

ink

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≼i is transitive

Equations

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

ink

@[simp]

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

ink

@[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 : α) : ↑(InitialSeg.trans f g) a = ↑g (↑f a)

ink

theorem InitialSeg.unique_of_trichotomous_of_irrefl {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrichotomous β s] [inst : IsIrrefl β s] : WellFounded r → Subsingleton (r ≼i s)

ink

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

Equations

• @InitialSeg.instSubsingletonInitialSeg = @InitialSeg.instSubsingletonInitialSeg.proof_1

ink

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

ink

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

ink

def InitialSeg.antisymm {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : 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

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

ink

@[simp]

theorem InitialSeg.antisymm_toFun {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) : ↑(RelIso.toRelEmbedding (InitialSeg.antisymm f g)).toEmbedding = ↑f

ink

@[simp]

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

ink

theorem InitialSeg.eq_or_principal {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ≼i s) : Function.Surjective ↑f ∨ ∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x

ink

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

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

ink

@[simp]

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

ink

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

Initial segment from an empty type.

Equations

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

ink

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

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

ink

@[simp]

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

Principal segments

Order embeddings whose range is a principal segment of s (i.e., an interval of the form (-∞, top)∞, 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≺i s. Principal segments are in particular initial segments.

ink

structure PrincipalSeg {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) extends RelEmbedding : Type (maxu_1u_2)

• The supremum of the principal segment

  top : β

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

  down' : ∀ (b : β), s b top ↔ ∃ a, ↑toRelEmbedding.toEmbedding a = b

If r is a relation on α and s in a relation on β, then f : r ≺i s≺i s is an order embedding whose range is an open interval (-∞, top)∞, top) for some element top of β. Such order embeddings are called principal segments

ink

def «term_≺i_» : Lean.TrailingParserDescr

If r is a relation on α and s in a relation on β, then f : r ≺i s≺i s is an order embedding whose range is an open interval (-∞, top)∞, 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))

ink

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

Equations

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

ink

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

Equations

• PrincipalSeg.instCoeFunPrincipalSegForAll = { coe := fun f => ↑f.toRelEmbedding.toEmbedding }

ink

@[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.toEmbedding a = b) : ↑{ toRelEmbedding := f, top := t, down' := o }.toRelEmbedding.toEmbedding = ↑f.toEmbedding

ink

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.toEmbedding a = b

ink

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

ink

theorem PrincipalSeg.init {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s) {a : α} {b : β} (h : s b (↑f.toRelEmbedding.toEmbedding a)) : ∃ a', ↑f.toRelEmbedding.toEmbedding a' = b

ink

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

A principal segment is in particular an initial segment.

Equations

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

ink

theorem PrincipalSeg.coe_coe_fn' {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s) : ↑{ toRelEmbedding := f.toRelEmbedding, init' := (_ : ∀ (x : α) (x_1 : β), s x_1 (↑f.toRelEmbedding.toEmbedding x) → ∃ a', ↑f.toRelEmbedding.toEmbedding a' = x_1) } = ↑f.toRelEmbedding.toEmbedding

ink

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

ink

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

ink

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

Equations

• @PrincipalSeg.instIsEmptyPrincipalSeg = @PrincipalSeg.instIsEmptyPrincipalSeg.proof_1

ink

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

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

ink

@[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 : α) : ↑(PrincipalSeg.ltLe f g).toRelEmbedding.toEmbedding a = ↑g (↑f.toRelEmbedding.toEmbedding a)

ink

@[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) : (PrincipalSeg.ltLe f g).top = ↑g f.top

ink

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

Composition of two principal segments as a principal segment

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

ink

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

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

ink

@[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.toEmbedding a = ↑g.toRelEmbedding.toEmbedding (↑(RelIso.toRelEmbedding f).toEmbedding a)

ink

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

ink

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

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

Equations

• @PrincipalSeg.instSubsingletonPrincipalSeg = @PrincipalSeg.instSubsingletonPrincipalSeg.proof_1

ink

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

ink

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

ink

def PrincipalSeg.ofElement {α : Type u_1} (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' := (_ : ∀ (x : α), r x a ↔ ∃ a, ↑(Subrel.relEmbedding r { b | r b a }).toEmbedding a = x) }

ink

@[simp]

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

ink

@[simp]

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

ink

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

Restrict the codomain of a principal segment

Equations

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

ink

@[simp]

theorem PrincipalSeg.codRestrict_apply {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : r ≺i s) (H : ∀ (a : α), ↑f.toRelEmbedding.toEmbedding a ∈ p) (H₂ : f.top ∈ p) (a : α) : ↑(PrincipalSeg.codRestrict p f H H₂).toRelEmbedding.toEmbedding a = { val := ↑f.toRelEmbedding.toEmbedding a, property := H a }

ink

@[simp]

theorem PrincipalSeg.codRestrict_top {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : r ≺i s) (H : ∀ (a : α), ↑f.toRelEmbedding.toEmbedding a ∈ p) (H₂ : f.top ∈ p) : (PrincipalSeg.codRestrict p f H H₂).top = { val := f.top, property := H₂ }

ink

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

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

Equations

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

ink

@[simp]

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

ink

def 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 PrincipalSeg.pemptyToPunit.proof_1

Properties of initial and principal segments

ink

noncomputable def InitialSeg.ltOrEq {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : 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.

ink

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

ink

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

ink

noncomputable def InitialSeg.leLT {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [inst : IsWellOrder β s] [inst : 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

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

ink

@[simp]

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

ink

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

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

ink

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

ink

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

ink

noncomputable def RelEmbedding.collapse {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : 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

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

ink

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