Initial and principal segments #
This file defines initial and principal segments.
Main definitions #
InitialSeg r s
: type of order embeddings ofr
intos
for which the range is an initial segment (i.e., ifb
belongs to the range, then anyb' < b
also belongs to the range). It is denoted byr ≼i s
.PrincipalSeg r s
: Type of order embeddings ofr
intos
for which the range is a principal segment, i.e., an interval of the form(-∞, top)
for some elementtop
. It is denoted byr ≺i s
.
Notations #
These notations belong to the InitialSeg
locale.
r ≼i s
: the type of initial segment embeddings ofr
intos
.r ≺i s
: the type of principal segment embeddings ofr
intos
.
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
.
- 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
The identity function shows that ≼i
is reflexive
Instances For
If we have order embeddings between α
and β
whose images are initial segments, and β
is a well-order then α
and β
are order-isomorphic.
Instances For
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.
- 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
The image of the order embedding is the set of elements
b
such thats 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
Given a well order s
, there is a most one principal segment embedding of r
into s
.
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.
Properties of initial and principal segments #
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
Composition of an initial segment taking values in a well order and a principal segment.
Instances For
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
Construct an initial segment from an order embedding into a well order, by collapsing it to fill the gaps.