# Documentation

Mathlib.Order.InitialSeg

# 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 :
Type (max u_4 u_5)
• toFun : αβ
• inj' : Function.Injective s.toFun
• map_rel_iff' : ∀ {a b : α}, s✝ (s.toEmbedding a) (s.toEmbedding b) r a b
• init' : ∀ (a : α) (b : β), s✝ b (s.toRelEmbedding a)a', s.toRelEmbedding a' = b

The order embedding is an initial segment

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.

Instances For

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.

Instances For
instance InitialSeg.instCoeInitialSegRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
Coe (r ≼i s) (r ↪r s)
instance InitialSeg.instEmbeddingLikeInitialSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
EmbeddingLike (r ≼i s) α β
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

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

The identity function shows that ≼i is reflexive

Instances For
instance InitialSeg.instInhabitedInitialSeg {α : Type u_1} (r : ααProp) :
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

Instances For
@[simp]
theorem InitialSeg.refl_apply {α : Type u_1} {r : ααProp} (x : α) :
↑() 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 : α) :
↑() a = g (f a)
instance InitialSeg.subsingleton_of_trichotomous_of_irrefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] [IsIrrefl β s] [] :
instance InitialSeg.instSubsingletonInitialSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] :
theorem InitialSeg.eq {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (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} [] (f : r ≼i s) (g : s ≼i r) :
def InitialSeg.antisymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (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.

Instances For
@[simp]
theorem InitialSeg.antisymm_toFun {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (f : r ≼i s) (g : s ≼i r) :
↑() = f
@[simp]
theorem InitialSeg.antisymm_symm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] [] (f : r ≼i s) (g : s ≼i r) :
theorem InitialSeg.eq_or_principal {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (f : r ≼i s) :
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

Instances For
@[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 : α) :
↑() a = { val := f a, property := H a }
def InitialSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [] :
r ≼i s

Initial segment from an empty type.

Instances For
def InitialSeg.leAdd {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :

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

Instances For
@[simp]
theorem InitialSeg.leAdd_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (a : α) :
↑() 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 :
Type (max u_4 u_5)
• toFun : αβ
• inj' : Function.Injective s.toFun
• map_rel_iff' : ∀ {a b : α}, s✝ (s.toEmbedding a) (s.toEmbedding b) r a b
• top : β

The supremum of the principal segment

• down' : ∀ (b : β), s✝ b s.top a, s.toRelEmbedding a = b

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

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

Instances For

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

Instances For
instance PrincipalSeg.instCoeOutPrincipalSegRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
CoeOut (r ≺i s) (r ↪r s)
instance PrincipalSeg.instCoeFunPrincipalSegForAll {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
CoeFun (r ≺i s) fun x => αβ
@[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.

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' := (_ : ∀ (x : α) (x_1 : β), s x_1 (f.toRelEmbedding x)a', f.toRelEmbedding a' = x_1) } = 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} [] (f : r ≺i r) :
instance PrincipalSeg.instIsEmptyPrincipalSeg {α : Type u_1} (r : ααProp) [] :
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

Instances For
@[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 : α) :
().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) :
().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

Instances For
@[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 : α) :
().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) :
().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

Instances For
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

Instances For
@[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 : α) :
().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) :
().top = g.top
instance PrincipalSeg.instSubsingletonPrincipalSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] :

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

theorem PrincipalSeg.top_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [] (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} [] (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

Instances For
@[simp]
theorem PrincipalSeg.ofElement_apply {α : Type u_4} (r : ααProp) (a : α) (b : {b | r b a}) :
().toRelEmbedding b = b
@[simp]
theorem PrincipalSeg.ofElement_top {α : Type u_4} (r : ααProp) (a : α) :
().top = a
@[simp]
theorem PrincipalSeg.subrelIso_symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≺i s) :
∀ (a : α), ↑() a = ↑(Equiv.setCongr (_ : Set.range f.toRelEmbedding = {b | s b f.top})) { val := f.toRelEmbedding a, property := (_ : y, f.toRelEmbedding y = 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.

Instances For
@[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 (↑() b) = b
@[simp]
theorem PrincipalSeg.subrelIso_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≺i s) (a : α) :
↑() { val := f.toRelEmbedding a, property := (_ : s (f.toRelEmbedding a) f.top a, f.toRelEmbedding a = f.toRelEmbedding a).mpr (_ : a, f.toRelEmbedding a = 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

Instances For
@[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 : α) :
().toRelEmbedding a = { val := f.toRelEmbedding a, property := H 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) :
().top = { val := f.top, property := H₂ }
def PrincipalSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) [] {b : β} (H : ∀ (b' : β), ¬s b' b) :
r ≺i s

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

Instances For
@[simp]
theorem PrincipalSeg.ofIsEmpty_top {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) [] {b : β} (H : ∀ (b' : β), ¬s b' b) :
().top = b
@[reducible]
def PrincipalSeg.pemptyToPunit :
EmptyRelation ≺i EmptyRelation

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

Instances For
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] :
∀ (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] :
∀ (α : Type u) (r : ααProp), r ≺i s

### Properties of initial and principal segments #

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

Instances For
theorem InitialSeg.ltOrEq_apply_left {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (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} [] (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} [] [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.

Instances For
@[simp]
theorem InitialSeg.leLT_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 : α) :
().toRelEmbedding a = g.toRelEmbedding (f a)
noncomputable def RelEmbedding.collapseF {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (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.

Instances For
theorem RelEmbedding.collapseF.lt {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (f : r ↪r s) {a : α} {a' : α} :
r a' as ↑() ↑()
theorem RelEmbedding.collapseF.not_lt {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (f : r ↪r s) (a : α) {b : β} (h : (a' : α) → r a' as (↑()) b) :
¬s b ↑()
noncomputable def RelEmbedding.collapse {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [] (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.

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