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≼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)∞, top)
for some elementtop
. It is denoted byr ≺i s≺i s
.
Notations #
These notations belong to the InitialSeg
locale.
r ≼i s≼i s
: the type of initial segment embeddings ofr
intos
.r ≺i s≺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≼i s
.
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
.
Instances For
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))
Equations
- InitialSeg.instEmbeddingLikeInitialSeg = EmbeddingLike.mk (_ : ∀ (f : r ≼i s), Function.Injective f.toRelEmbedding.toEmbedding.toFun)
Equations
- InitialSeg.instInhabitedInitialSeg r = { default := InitialSeg.refl r }
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.
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.
The supremum of the principal segment
top : β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≺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
Instances For
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))
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.
Composition of two principal segments as a principal segment
Equations
- One or more equations did not get rendered due to their size.
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.
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.
Given a well order s
, there is a most one principal segment embedding of r
into s
.
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) }
Restrict the codomain of a principal segment
Equations
- One or more equations did not get rendered due to their size.
Principal segment from the empty relation on pempty
to the empty relation on punit
.
Equations
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).
Equations
- One or more equations did not get rendered due to their size.
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
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.
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.