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
.
The lemmas Ordinal.type_le_iff
and Ordinal.type_lt_iff
tell us that ≼i
corresponds to the ≤
relation on ordinals, while ≺i
corresponds to the <
relation. This prompts us to think of
PrincipalSeg
as a "strict" version of InitialSeg
.
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
.α ≤i β
is an abbreviation for(· < ·) ≼i (· < ·)
.α <i β
is an abbreviation for(· < ·) ≺i (· < ·)
.
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
.
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
- mem_range_of_rel' : ∀ (a : α) (b : β), s b (self.toRelEmbedding a) → b ∈ Set.range ⇑self.toRelEmbedding
The order embedding is an initial segment
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
.
Equations
- «term_≼i_» = Lean.ParserDescr.trailingNode `«term_≼i_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼i ") (Lean.ParserDescr.cat `term 26))
Instances For
An InitialSeg
between the <
relations of two types.
Equations
- «term_≤i_» = Lean.ParserDescr.trailingNode `«term_≤i_» 25 24 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤i ") (Lean.ParserDescr.cat `term 25))
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
An initial segment embedding between the <
relations of two partial orders is an order
embedding.
Equations
- f.toOrderEmbedding = f.orderEmbeddingOfLTEmbedding
Instances For
Equations
- ⋯ = ⋯
Alias of InitialSeg.mem_range_of_rel
.
An order isomorphism is an initial segment
Equations
- InitialSeg.ofIso f = { toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := ⋯ }
Instances For
The identity function shows that ≼i
is reflexive
Equations
- InitialSeg.refl r = { toRelEmbedding := RelEmbedding.refl r, mem_range_of_rel' := ⋯ }
Instances For
Equations
- InitialSeg.instInhabited r = { default := InitialSeg.refl r }
Composition of functions shows that ≼i
is transitive
Equations
- f.trans g = { toRelEmbedding := f.trans g.toRelEmbedding, mem_range_of_rel' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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' := ⋯ }
Instances For
Restrict the codomain of an initial segment
Equations
- InitialSeg.codRestrict p f H = { toRelEmbedding := RelEmbedding.codRestrict p f.toRelEmbedding H, mem_range_of_rel' := ⋯ }
Instances For
Initial segment from an empty type.
Equations
- InitialSeg.ofIsEmpty r s = { toRelEmbedding := RelEmbedding.ofIsEmpty r s, mem_range_of_rel' := ⋯ }
Instances For
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' := ⋯, mem_range_of_rel' := ⋯ }
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.
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
The range of the order embedding is the set of elements
b
such thats b top
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
Equations
- «term_≺i_» = Lean.ParserDescr.trailingNode `«term_≺i_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺i ") (Lean.ParserDescr.cat `term 26))
Instances For
A PrincipalSeg
between the <
relations of two types.
Equations
- «term_<i_» = Lean.ParserDescr.trailingNode `«term_<i_» 25 24 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <i ") (Lean.ParserDescr.cat `term 25))
Instances For
Alias of PrincipalSeg.exists_eq_iff_rel
.
A principal segment is the same as a non-surjective initial segment.
Equations
- f.toPrincipalSeg hf = { toRelEmbedding := f.toRelEmbedding, top := Classical.choose ⋯, mem_range_iff_rel' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
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, mem_range_iff_rel' := ⋯ }
Instances For
Composition of two principal segments as a principal segment
Equations
- f.trans g = f.ltLe { toRelEmbedding := g.toRelEmbedding, mem_range_of_rel' := ⋯ }
Instances For
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, mem_range_iff_rel' := ⋯ }
Instances For
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, mem_range_iff_rel' := ⋯ }
Instances For
Given a well order s
, there is a most one principal segment embedding of r
into s
.
Equations
- ⋯ = ⋯
Alias of PrincipalSeg.top_rel_top
.
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, mem_range_iff_rel' := ⋯ }
Instances For
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
Instances For
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₂⟩, mem_range_iff_rel' := ⋯ }
Instances For
Principal segment from an empty type into a type with a minimal element.
Equations
- PrincipalSeg.ofIsEmpty r H = { toRelEmbedding := RelEmbedding.ofIsEmpty r s, top := b, mem_range_iff_rel' := ⋯ }
Instances For
Principal segment from the empty relation on PEmpty
to the empty relation on PUnit
.
Equations
- PrincipalSeg.pemptyToPunit = PrincipalSeg.ofIsEmpty EmptyRelation ⋯
Instances For
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
- f.ltOrEq = if h : Function.Surjective ⇑f then Sum.inr (RelIso.ofSurjective f.toRelEmbedding h) else Sum.inl (f.toPrincipalSeg h)
Instances For
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
Instances For
Construct an initial segment embedding r ≼i s
by "filling in the gaps". That is, each
subsequent element in α
is mapped to the least element in β
that hasn't been used yet.
This construction is guaranteed to work as long as there exists some relation embedding r ↪r s
.
Equations
- f.collapse = { toRelEmbedding := RelEmbedding.ofMonotone (fun (a : α) => ↑(collapseF f a)) ⋯, mem_range_of_rel' := ⋯ }
Instances For
For any two well orders, one is an initial segment of the other.
Equations
- One or more equations did not get rendered due to their size.