mathlib3 documentation

order.initial_seg

Initial and principal segments #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines initial and principal segments.

Main definitions #

Notations #

These notations belong to the initial_seg locale.

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 initial_seg r s, and denoted by r ≼i s.

structure initial_seg {α : Type u_4} {β : Type u_5} (r : α α Prop) (s : β β Prop) :
Type (max u_4 u_5)

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 initial_seg
@[protected, instance]
def initial_seg.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
Equations
@[protected, instance]
def initial_seg.embedding_like {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
Equations
@[ext]
theorem initial_seg.ext {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} {f g : initial_seg r s} (h : (x : α), f x = g x) :
f = g
@[simp]
theorem initial_seg.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ↪r s) (o : (a : α) (b : β), s b (f a) ( (a' : α), f a' = b)) :
@[simp]
theorem initial_seg.coe_fn_to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : initial_seg r s) :
@[simp]
theorem initial_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : initial_seg r s) :
theorem initial_seg.init {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : initial_seg r s) {a : α} {b : β} :
s b (f a) ( (a' : α), f a' = b)
theorem initial_seg.map_rel_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : initial_seg r s) {a b : α} :
s (f a) (f b) r a b
theorem initial_seg.init_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : initial_seg r s) {a : α} {b : β} :
s b (f a) (a' : α), f a' = b r a' a
def initial_seg.of_iso {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : r ≃r s) :

An order isomorphism is an initial segment

Equations
@[protected, refl]
def initial_seg.refl {α : Type u_1} (r : α α Prop) :

The identity function shows that ≼i is reflexive

Equations
@[protected, instance]
def initial_seg.inhabited {α : Type u_1} (r : α α Prop) :
Equations
@[protected, trans]
def initial_seg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : initial_seg r s) (g : initial_seg s t) :

Composition of functions shows that ≼i is transitive

Equations
@[simp]
theorem initial_seg.refl_apply {α : Type u_1} {r : α α Prop} (x : α) :
@[simp]
theorem initial_seg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : initial_seg r s) (g : initial_seg s t) (a : α) :
(f.trans g) a = g (f a)
@[protected, instance]
def initial_seg.subsingleton_of_trichotomous_of_irrefl {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_trichotomous β s] [is_irrefl β s] [is_well_founded α r] :
@[protected, instance]
def initial_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] :
@[protected]
theorem initial_seg.eq {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f g : initial_seg r s) (a : α) :
f a = g a
theorem initial_seg.antisymm.aux {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order α r] (f : initial_seg r s) (g : initial_seg s r) :
def initial_seg.antisymm {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : initial_seg r s) (g : initial_seg s 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
@[simp]
theorem initial_seg.antisymm_to_fun {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : initial_seg r s) (g : initial_seg s r) :
@[simp]
theorem initial_seg.antisymm_symm {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order α r] [is_well_order β s] (f : initial_seg r s) (g : initial_seg s r) :
theorem initial_seg.eq_or_principal {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : initial_seg r s) :
function.surjective f (b : β), (x : β), s x b (y : α), f y = x
def initial_seg.cod_restrict {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (p : set β) (f : initial_seg r s) (H : (a : α), f a p) :

Restrict the codomain of an initial segment

Equations
@[simp]
theorem initial_seg.cod_restrict_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (p : set β) (f : initial_seg r s) (H : (a : α), f a p) (a : α) :
def initial_seg.of_is_empty {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) [is_empty α] :

Initial segment from an empty type.

Equations
def initial_seg.le_add {α : 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.

Equations
@[simp]
theorem initial_seg.le_add_apply {α : Type u_1} {β : Type u_2} (r : α α Prop) (s : β β Prop) (a : α) :
@[protected]
theorem initial_seg.acc {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : initial_seg r 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 principal_seg r s, and denoted by r ≺i s. Principal segments are in particular initial segments.

@[nolint]
structure principal_seg {α : Type u_4} {β : Type u_5} (r : α α Prop) (s : β β Prop) :
Type (max u_4 u_5)

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 principal_seg
@[protected, instance]
def principal_seg.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
Equations
@[protected, instance]
def principal_seg.has_coe_to_fun {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} :
has_coe_to_fun (principal_seg r s) (λ (_x : principal_seg r s), α β)
Equations
@[simp]
theorem principal_seg.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) :
{to_rel_embedding := f, top := t, down' := o} = f
@[simp]
theorem principal_seg.coe_fn_to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : principal_seg r s) :
@[simp]
theorem principal_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : principal_seg r s) :
theorem principal_seg.down {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : principal_seg r s) {b : β} :
s b f.top (a : α), f a = b
theorem principal_seg.lt_top {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : principal_seg r s) (a : α) :
s (f a) f.top
theorem principal_seg.init {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_trans β s] (f : principal_seg r s) {a : α} {b : β} (h : s b (f a)) :
(a' : α), f a' = b
@[protected, instance]
def principal_seg.has_coe_initial_seg {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_trans β s] :

A principal segment is in particular an initial segment.

Equations
theorem principal_seg.coe_coe_fn' {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_trans β s] (f : principal_seg r s) :
theorem principal_seg.init_iff {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_trans β s] (f : principal_seg r s) {a : α} {b : β} :
s b (f a) (a' : α), f a' = b r a' a
theorem principal_seg.irrefl {α : Type u_1} {r : α α Prop} [is_well_order α r] (f : principal_seg r r) :
@[protected, instance]
def principal_seg.is_empty {α : Type u_1} (r : α α Prop) [is_well_order α r] :
def principal_seg.lt_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : principal_seg r s) (g : initial_seg s t) :

Composition of a principal segment with an initial segment, as a principal segment

Equations
@[simp]
theorem principal_seg.lt_le_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : principal_seg r s) (g : initial_seg s t) (a : α) :
(f.lt_le g) a = g (f a)
@[simp]
theorem principal_seg.lt_le_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : principal_seg r s) (g : initial_seg s t) :
(f.lt_le g).top = g f.top
@[protected, trans]
def principal_seg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} [is_trans γ t] (f : principal_seg r s) (g : principal_seg s t) :

Composition of two principal segments as a principal segment

Equations
@[simp]
theorem principal_seg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} [is_trans γ t] (f : principal_seg r s) (g : principal_seg s t) (a : α) :
(f.trans g) a = g (f a)
@[simp]
theorem principal_seg.trans_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} [is_trans γ t] (f : principal_seg r s) (g : principal_seg s t) :
(f.trans g).top = g f.top
def principal_seg.equiv_lt {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : r ≃r s) (g : principal_seg s t) :

Composition of an order isomorphism with a principal segment, as a principal segment

Equations
def principal_seg.lt_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : principal_seg r s) (g : s ≃r t) :

Composition of a principal segment with an order isomorphism, as a principal segment

Equations
@[simp]
theorem principal_seg.equiv_lt_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : r ≃r s) (g : principal_seg s t) (a : α) :
@[simp]
theorem principal_seg.equiv_lt_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : r ≃r s) (g : principal_seg s t) :
@[protected, instance]
def principal_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] :

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

theorem principal_seg.top_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} [is_well_order γ t] (e : r ≃r s) (f : principal_seg r t) (g : principal_seg s t) :
f.top = g.top
theorem principal_seg.top_lt_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} [is_well_order γ t] (f : principal_seg r s) (g : principal_seg s t) (h : principal_seg r t) :
t h.top g.top
def principal_seg.of_element {α : Type u_1} (r : α α Prop) (a : α) :
principal_seg (subrel r {b : α | r b a}) r

Any element of a well order yields a principal segment

Equations
@[simp]
theorem principal_seg.of_element_apply {α : Type u_1} (r : α α Prop) (a : α) (b : {b : α | r b a}) :
@[simp]
theorem principal_seg.of_element_top {α : Type u_1} (r : α α Prop) (a : α) :
noncomputable def principal_seg.subrel_iso {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : principal_seg r 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.

Equations
@[simp]
theorem principal_seg.subrel_iso_symm_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : principal_seg r s) (ᾰ : α) :
(f.subrel_iso.symm) ᾰ = f ᾰ, _⟩
@[simp]
theorem principal_seg.apply_subrel_iso {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : principal_seg r s) (b : {b : β | s b f.top}) :
@[simp]
theorem principal_seg.subrel_iso_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (f : principal_seg r s) (a : α) :
(f.subrel_iso) f a, _⟩ = a
def principal_seg.cod_restrict {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (p : set β) (f : principal_seg r s) (H : (a : α), f a p) (H₂ : f.top p) :

Restrict the codomain of a principal segment

Equations
@[simp]
theorem principal_seg.cod_restrict_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (p : set β) (f : principal_seg r s) (H : (a : α), f a p) (H₂ : f.top p) (a : α) :
(principal_seg.cod_restrict p f H H₂) a = f a, _⟩
@[simp]
theorem principal_seg.cod_restrict_top {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} (p : set β) (f : principal_seg r s) (H : (a : α), f a p) (H₂ : f.top p) :
(principal_seg.cod_restrict p f H H₂).top = f.top, H₂⟩
def principal_seg.of_is_empty {α : Type u_1} {β : Type u_2} {s : β β Prop} (r : α α Prop) [is_empty α] {b : β} (H : (b' : β), ¬s b' b) :

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

Equations
@[simp]
theorem principal_seg.of_is_empty_top {α : Type u_1} {β : Type u_2} {s : β β Prop} (r : α α Prop) [is_empty α] {b : β} (H : (b' : β), ¬s b' b) :
@[reducible]

Principal segment from the empty relation on pempty to the empty relation on punit.

Equations
@[protected]
theorem principal_seg.acc {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_trans β s] (f : principal_seg r s) (a : α) :
acc r a acc s (f a)
theorem well_founded_iff_well_founded_subrel {β : Type u_1} {s : β β Prop} [is_trans β s] :
well_founded s (b : β), well_founded (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 well_founded_iff_principal_seg {β : Type u} {s : β β Prop} [is_trans β s] :
well_founded s (α : Type u) (r : α α Prop), principal_seg r s well_founded r

Properties of initial and principal segments #

noncomputable def initial_seg.lt_or_eq {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : initial_seg 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
theorem initial_seg.lt_or_eq_apply_left {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : initial_seg r s) (g : principal_seg r s) (a : α) :
g a = f a
theorem initial_seg.lt_or_eq_apply_right {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : initial_seg r s) (g : r ≃r s) (a : α) :
g a = f a
noncomputable def initial_seg.le_lt {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} [is_well_order β s] [is_trans γ t] (f : initial_seg r s) (g : principal_seg s t) :

Composition of an initial segment taking values in a well order and a principal segment.

Equations
@[simp]
theorem initial_seg.le_lt_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} [is_well_order β s] [is_trans γ t] (f : initial_seg r s) (g : principal_seg s t) (a : α) :
(f.le_lt g) a = g (f a)
noncomputable def rel_embedding.collapse_F {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (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.

Equations
  • f.collapse_F = _.fix (λ (a : α) (IH : Π (y : α), r y a {b // ¬s (f y) b}), let S : set β := {b : β | (a_1 : α) (h : r a_1 a), s (IH a_1 h).val b} in rel_embedding.collapse_F._proof_2.min S _, _⟩)
theorem rel_embedding.collapse_F.lt {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : r ↪r s) {a a' : α} :
r a' a s (f.collapse_F a').val (f.collapse_F a).val
theorem rel_embedding.collapse_F.not_lt {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : r ↪r s) (a : α) {b : β} (h : (a' : α), r a' a s (f.collapse_F a').val b) :
¬s b (f.collapse_F a).val
noncomputable def rel_embedding.collapse {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : r ↪r s) :

Construct an initial segment from an order embedding into a well order, by collapsing it to fill the gaps.

Equations
theorem rel_embedding.collapse_apply {α : Type u_1} {β : Type u_2} {r : α α Prop} {s : β β Prop} [is_well_order β s] (f : r ↪r s) (a : α) :