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 #

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

source

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

Type (max u_4 u_5)

to_rel_embedding : r ↪r s
init' : ∀ (a : α) (b : β), s b (⇑(self.to_rel_embedding) a) → (∃ (a' : α), ⇑(self.to_rel_embedding) a' = b)

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

initial_seg.has_sizeof_inst
initial_seg.rel_embedding.has_coe
initial_seg.embedding_like
initial_seg.inhabited
initial_seg.subsingleton_of_trichotomous_of_irrefl
initial_seg.subsingleton
principal_seg.has_coe_initial_seg

source

@[protected, instance]

def initial_seg.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

has_coe (initial_seg r s) (r ↪r s)

Equations

initial_seg.rel_embedding.has_coe = {coe := initial_seg.to_rel_embedding s}

source

@[protected, instance]

def initial_seg.embedding_like {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

embedding_like (initial_seg r s) α β

Equations

initial_seg.embedding_like = {coe := λ (f : initial_seg r s), f.to_rel_embedding.to_embedding.to_fun, coe_injective' := _, injective' := _}

source

@[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

source

@[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)) :

⇑{to_rel_embedding := f, init' := o} = ⇑f

source

@[simp]

theorem initial_seg.coe_fn_to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : initial_seg r s) :

⇑(f.to_rel_embedding) = ⇑f

source

@[simp]

theorem initial_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : initial_seg r s) :

⇑↑f = ⇑f

source

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)

source

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

source

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

source

def initial_seg.of_iso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) :

initial_seg r s

An order isomorphism is an initial segment

Equations

initial_seg.of_iso f = {to_rel_embedding := ↑f, init' := _}

source

@[protected, refl]

def initial_seg.refl {α : Type u_1} (r : α → α → Prop) :

initial_seg r r

The identity function shows that ≼i is reflexive

Equations

initial_seg.refl r = {to_rel_embedding := rel_embedding.refl r, init' := _}

source

@[protected, instance]

def initial_seg.inhabited {α : Type u_1} (r : α → α → Prop) :

inhabited (initial_seg r r)

Equations

initial_seg.inhabited r = {default := initial_seg.refl r}

source

@[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) :

initial_seg r t

Composition of functions shows that ≼i is transitive

Equations

f.trans g = {to_rel_embedding := f.to_rel_embedding.trans g.to_rel_embedding, init' := _}

source

@[simp]

theorem initial_seg.refl_apply {α : Type u_1} {r : α → α → Prop} (x : α) :

⇑(initial_seg.refl r) x = x

source

@[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)

source

@[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] :

subsingleton (initial_seg r s)

source

@[protected, instance]

def initial_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] :

subsingleton (initial_seg r s)

source

@[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

source

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) :

function.left_inverse ⇑g ⇑f

source

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

f.antisymm g = {to_equiv := {to_fun := ⇑f, inv_fun := ⇑g, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[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) :

⇑(f.antisymm g) = ⇑f

source

@[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) :

(f.antisymm g).symm = g.antisymm f

source

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

source

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) :

initial_seg r (subrel s p)

Restrict the codomain of an initial segment

Equations

initial_seg.cod_restrict p f H = {to_rel_embedding := rel_embedding.cod_restrict p ↑f H, init' := _}

source

@[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 : α) :

⇑(initial_seg.cod_restrict p f H) a = ⟨⇑f a, _⟩

source

def initial_seg.of_is_empty {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [is_empty α] :

initial_seg r s

Initial segment from an empty type.

Equations

initial_seg.of_is_empty r s = {to_rel_embedding := rel_embedding.of_is_empty r s _inst_1, init' := _}

source

def initial_seg.le_add {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) :

initial_seg r (sum.lex r s)

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

Equations

initial_seg.le_add r s = {to_rel_embedding := {to_embedding := {to_fun := sum.inl β, inj' := _}, map_rel_iff' := _}, init' := _}

source

@[simp]

theorem initial_seg.le_add_apply {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (a : α) :

⇑(initial_seg.le_add r s) a = sum.inl a

source

@[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.

source

@[nolint]

structure principal_seg {α : Type u_4} {β : Type u_5} (r : α → α → Prop) (s : β → β → Prop) :

Type (max u_4 u_5)

to_rel_embedding : r ↪r s
top : β
down' : ∀ (b : β), s b self.top ↔ ∃ (a : α), ⇑(self.to_rel_embedding) a = b

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

source

@[protected, instance]

def principal_seg.rel_embedding.has_coe {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} :

has_coe (principal_seg r s) (r ↪r s)

Equations

principal_seg.rel_embedding.has_coe = {coe := principal_seg.to_rel_embedding s}

source

@[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

principal_seg.has_coe_to_fun = {coe := λ (f : principal_seg r s), ⇑f}

source

@[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

source

@[simp]

theorem principal_seg.coe_fn_to_rel_embedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : principal_seg r s) :

⇑(f.to_rel_embedding) = ⇑f

source

@[simp]

theorem principal_seg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : principal_seg r s) :

⇑↑f = ⇑f

source

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

source

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

source

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

source

@[protected, instance]

def principal_seg.has_coe_initial_seg {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trans β s] :

has_coe (principal_seg r s) (initial_seg r s)

A principal segment is in particular an initial segment.

Equations

principal_seg.has_coe_initial_seg = {coe := λ (f : principal_seg r s), {to_rel_embedding := f.to_rel_embedding, init' := _}}

source

theorem principal_seg.coe_coe_fn' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_trans β s] (f : principal_seg r s) :

⇑↑f = ⇑f

source

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

source

theorem principal_seg.irrefl {α : Type u_1} {r : α → α → Prop} [is_well_order α r] (f : principal_seg r r) :

false

source

@[protected, instance]

def principal_seg.is_empty {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

is_empty (principal_seg r r)

source

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) :

principal_seg r t

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

Equations

f.lt_le g = {to_rel_embedding := ↑f.trans ↑g, top := ⇑g f.top, down' := _}

source

@[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)

source

@[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

source

@[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) :

principal_seg r t

Composition of two principal segments as a principal segment

Equations

f.trans g = f.lt_le ↑g

source

@[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)

source

@[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

source

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) :

principal_seg r t

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

Equations

principal_seg.equiv_lt f g = {to_rel_embedding := ↑f.trans ↑g, top := g.top, down' := _}

source

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) :

principal_seg r t

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

Equations

f.lt_equiv g = {to_rel_embedding := ↑f.trans ↑g, top := ⇑g f.top, down' := _}

source

@[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 : α) :

⇑(principal_seg.equiv_lt f g) a = ⇑g (⇑f a)

source

@[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) :

(principal_seg.equiv_lt f g).top = g.top

source

@[protected, instance]

def principal_seg.subsingleton {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] :

subsingleton (principal_seg r s)

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

source

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

source

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

source

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

principal_seg.of_element r a = {to_rel_embedding := subrel.rel_embedding r {b : α | r b a}, top := a, down' := _}

source

@[simp]

theorem principal_seg.of_element_apply {α : Type u_1} (r : α → α → Prop) (a : α) (b : ↥{b : α | r b a}) :

⇑(principal_seg.of_element r a) b = b.val

source

@[simp]

theorem principal_seg.of_element_top {α : Type u_1} (r : α → α → Prop) (a : α) :

(principal_seg.of_element r a).top = a

source

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

f.subrel_iso = {to_equiv := (equiv.of_injective ⇑f _).trans (equiv.set_congr _), map_rel_iff' := _}.symm

source

@[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 ᾰ, _⟩

source

@[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}) :

⇑f (⇑(f.subrel_iso) b) = ↑b

source

@[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

source

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) :

principal_seg r (subrel s p)

Restrict the codomain of a principal segment

Equations

principal_seg.cod_restrict p f H H₂ = {to_rel_embedding := rel_embedding.cod_restrict p ↑f H, top := ⟨f.top, H₂⟩, down' := _}

source

@[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, _⟩

source

@[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₂⟩

source

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_seg r s

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

Equations

principal_seg.of_is_empty r H = {to_rel_embedding := {to_embedding := (rel_embedding.of_is_empty r s).to_embedding, map_rel_iff' := _}, top := b, down' := _}

source

@[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) :

(principal_seg.of_is_empty r H).top = b

source

@[reducible]

def principal_seg.pempty_to_punit :

principal_seg empty_relation empty_relation

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

Equations

principal_seg.pempty_to_punit = principal_seg.of_is_empty empty_relation principal_seg.pempty_to_punit._proof_1

source

@[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)

source

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.

source

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 #

source

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) :

principal_seg r 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).

Equations

f.lt_or_eq = dite (function.surjective ⇑f) (λ (h : function.surjective ⇑f), sum.inr (rel_iso.of_surjective ↑f h)) (λ (h : ¬function.surjective ⇑f), sum.inl {to_rel_embedding := ↑f, top := classical.some _, down' := _})

source

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

source

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

source

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) :

principal_seg r t

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

Equations

f.le_lt g = initial_seg.le_lt._match_1 g f.lt_or_eq
initial_seg.le_lt._match_1 g (sum.inr f') = principal_seg.equiv_lt f' g
initial_seg.le_lt._match_1 g (sum.inl f') = f'.trans g

source

@[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)

source

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 _, _⟩)

source

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

source

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

source

noncomputable def rel_embedding.collapse {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [is_well_order β s] (f : r ↪r s) :

initial_seg r s

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

Equations

f.collapse = {to_rel_embedding := rel_embedding.of_monotone (λ (a : α), (f.collapse_F a).val) _, init' := _}

source

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

⇑(f.collapse) a = (f.collapse_F a).val