Mathlib.Order.InitialSeg

Module docstring

{"# Initial and principal segments

This file defines initial and principal segment embeddings. Though these definitions make sense for arbitrary relations, they're intended for use with well orders.

An initial segment is simply a lower set, i.e. if x belongs to the range, then any y < x also belongs to the range. A principal segment is a set of the form Set.Iio x for some x.

An initial segment embedding r ≼i s is an order embedding r ↪ s such that its range is an initial segment. Likewise, a principal segment embedding r ≺i s has a principal segment for a range.

Main definitions

InitialSeg r s: Type of initial segment embeddings of r into s , denoted by r ≼i s.
PrincipalSeg r s: Type of principal segment embeddings of r into s , denoted by r ≺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 of r into s.
r ≺i s: the type of principal segment embeddings of r into s.
α ≤i β is an abbreviation for (· < ·) ≼i (· < ·).
α <i β is an abbreviation for (· < ·) ≺i (· < ·). ","### Initial segment embeddings ","### Principal segments ","### Properties of initial and principal segments ","### Initial or principal segments with < "}

InitialSeg structure

{α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends r ↪r s

Full source

/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≼i s` is an order
embedding whose `Set.range` is a lower set. That is, whenever `b < f a` in `β` then `b` is in the
range of `f`. -/
structure InitialSeg {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends r ↪r s where
  /-- The order embedding is an initial segment -/
  mem_range_of_rel' : ∀ a b, s b (toRelEmbedding a) → b ∈ Set.range toRelEmbedding

Initial Segment Embedding

Informal description

An initial segment embedding between two relations `r` on `α` and `s` on `β` is an order embedding `f : r ↪r s` where the range of `f` forms a lower set. This means that for any elements `a ∈ α` and `b ∈ β`, if `b` is related to `f(a)` under `s` (i.e., `b < f(a)`), then `b` must be in the range of `f`.

InitialSeg.term_≼i_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped[InitialSeg] infixl:25 " ≼i " => InitialSeg

Initial segment embedding notation

Informal description

The notation `r ≼i s` represents the type of initial segment embeddings from a relation `r` on `α` to a relation `s` on `β`. An initial segment embedding is an order embedding whose range forms an initial segment, meaning that if an element is in the range, then all elements below it (with respect to `s`) are also in the range.

term_≤i_ definition

: Lean.TrailingParserDescr✝

Full source

/-- An `InitialSeg` between the `<` relations of two types. -/
notation:25 α:24 " ≤i " β:25 => @InitialSeg α β (· < ·) (· < ·)

Initial segment embedding between strict orders

Informal description

The notation `α ≤i β` represents an initial segment embedding between the strict order relations `<` on two types `α` and `β`. This means there exists an order embedding from `α` to `β` whose range is an initial segment in `β` (i.e., if an element is in the range, all elements less than it are also in the range).

InitialSeg.instCoeRelEmbedding instance

: Coe (r ≼i s) (r ↪r s)

Full source

instance : Coe (r ≼i s) (r ↪r s) :=
  ⟨InitialSeg.toRelEmbedding⟩

Initial Segment Embedding as Relation Embedding

Informal description

Every initial segment embedding $r \preceq_i s$ can be viewed as a relation embedding $r \hookrightarrow_r s$.

InitialSeg.instFunLike instance

: FunLike (r ≼i s) α β

Full source

instance : FunLike (r ≼i s) α β where
  coe f := f.toFun
  coe_injective' := by
    rintro ⟨f, hf⟩ ⟨g, hg⟩ h
    congr with x
    exact congr_fun h x

Function-Like Structure on Initial Segment Embeddings

Informal description

For any two relations $r$ on $\alpha$ and $s$ on $\beta$, the type of initial segment embeddings $r \preceq_i s$ has a function-like structure, meaning its elements can be coerced to functions from $\alpha$ to $\beta$.

InitialSeg.instEmbeddingLike instance

: EmbeddingLike (r ≼i s) α β

Full source

instance : EmbeddingLike (r ≼i s) α β where
  injective' f := f.inj'

Embedding-Like Structure on Initial Segment Embeddings

Informal description

For any two relations $r$ on $\alpha$ and $s$ on $\beta$, the type of initial segment embeddings $r \preceq_i s$ has an embedding-like structure, meaning its elements can be coerced to injective functions from $\alpha$ to $\beta$ that preserve the relation structure.

InitialSeg.instRelHomClass instance

: RelHomClass (r ≼i s) r s

Full source

instance : RelHomClass (r ≼i s) r s where
  map_rel f := f.map_rel_iff.2

Initial Segment Embeddings as Relation Homomorphisms

Informal description

For any two relations $r$ on $\alpha$ and $s$ on $\beta$, the type of initial segment embeddings $r \preceq_i s$ forms a class of relation homomorphisms, meaning each embedding $f : r \preceq_i s$ preserves the relations: for any $a, b \in \alpha$, $r(a, b)$ holds if and only if $s(f(a), f(b))$ holds.

InitialSeg.toOrderEmbedding definition

[PartialOrder α] [PartialOrder β] (f : α ≤i β) : α ↪o β

Full source

/-- An initial segment embedding between the `<` relations of two partial orders is an order
embedding. -/
def toOrderEmbedding [PartialOrder α] [PartialOrder β] (f : α ≤i β) : α ↪o β :=
  f.orderEmbeddingOfLTEmbedding

Order embedding induced by an initial segment embedding

Informal description

Given a partial order $\alpha$ and a partial order $\beta$, any initial segment embedding $f : \alpha \leq_i \beta$ (i.e., an order embedding where the range is a lower set) induces an order embedding from $\alpha$ to $\beta$ with respect to the non-strict order $\leq$.

InitialSeg.toOrderEmbedding_apply theorem

[PartialOrder α] [PartialOrder β] (f : α ≤i β) (x : α) : f.toOrderEmbedding x = f x

Full source

@[simp]
theorem toOrderEmbedding_apply [PartialOrder α] [PartialOrder β] (f : α ≤i β) (x : α) :
    f.toOrderEmbedding x = f x :=
  rfl

Equality of Order Embedding Application in Initial Segment Embedding

Informal description

Given a partial order $\alpha$ and a partial order $\beta$, for any initial segment embedding $f : \alpha \leq_i \beta$ and any element $x \in \alpha$, the application of the induced order embedding $f.toOrderEmbedding$ to $x$ equals the application of $f$ to $x$, i.e., $f.toOrderEmbedding(x) = f(x)$.

InitialSeg.coe_toOrderEmbedding theorem

[PartialOrder α] [PartialOrder β] (f : α ≤i β) : (f.toOrderEmbedding : α → β) = f

Full source

@[simp]
theorem coe_toOrderEmbedding [PartialOrder α] [PartialOrder β] (f : α ≤i β) :
    (f.toOrderEmbedding : α → β) = f :=
  rfl

Coercion of Initial Segment Embedding to Order Embedding Equals Original Function

Informal description

Let $\alpha$ and $\beta$ be partial orders, and let $f : \alpha \leq_i \beta$ be an initial segment embedding. Then the underlying function of the order embedding $f.toOrderEmbedding$ is equal to $f$ itself.

InitialSeg.instOrderHomClassLt instance

[PartialOrder α] [PartialOrder β] : OrderHomClass (α ≤i β) α β

Full source

instance [PartialOrder α] [PartialOrder β] : OrderHomClass (α ≤i β) α β where
  map_rel f := f.toOrderEmbedding.map_rel_iff.2

Initial Segment Embeddings are Order-Preserving

Informal description

For any two partially ordered sets $\alpha$ and $\beta$, the type of initial segment embeddings $\alpha \leq_i \beta$ forms an order homomorphism class, meaning that every initial segment embedding preserves the order relation.

InitialSeg.ext theorem

{f g : r ≼i s} (h : ∀ x, f x = g x) : f = g

Full source

@[ext] lemma ext {f g : r ≼i s} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality of Initial Segment Embeddings

Informal description

Let $r$ be a relation on $\alpha$ and $s$ a relation on $\beta$. For any two initial segment embeddings $f, g \colon r \preceq_i s$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

InitialSeg.coe_coe_fn theorem

(f : r ≼i s) : ((f : r ↪r s) : α → β) = f

Full source

@[simp]
theorem coe_coe_fn (f : r ≼i s) : ((f : r ↪r s) : α → β) = f :=
  rfl

Coercion Consistency for Initial Segment Embeddings

Informal description

For any initial segment embedding $f : r \preceq_i s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the underlying function of $f$ (when viewed as a relation embedding $r \hookrightarrow s$) is equal to $f$ itself when coerced to a function from $\alpha$ to $\beta$.

InitialSeg.mem_range_of_rel theorem

(f : r ≼i s) {a : α} {b : β} : s b (f a) → b ∈ Set.range f

Full source

theorem mem_range_of_rel (f : r ≼i s) {a : α} {b : β} : s b (f a) → b ∈ Set.range f :=
  f.mem_range_of_rel' _ _

Range Membership Property of Initial Segment Embeddings

Informal description

Let $r$ be a relation on $\alpha$ and $s$ a relation on $\beta$. For any initial segment embedding $f \colon r \preceq_i s$ and elements $a \in \alpha$, $b \in \beta$, if $b$ is related to $f(a)$ under $s$ (i.e., $b \mathrel{s} f(a)$), then $b$ belongs to the range of $f$.

InitialSeg.map_rel_iff theorem

{a b : α} (f : r ≼i s) : s (f a) (f b) ↔ r a b

Full source

theorem map_rel_iff {a b : α} (f : r ≼i s) : s (f a) (f b) ↔ r a b :=
  f.map_rel_iff'

Initial Segment Embedding Preserves Relation

Informal description

For any initial segment embedding $f \colon r \preceq_i s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $a, b \in \alpha$, we have $s(f(a), f(b))$ if and only if $r(a, b)$.

InitialSeg.inj theorem

(f : r ≼i s) {a b : α} : f a = f b ↔ a = b

Full source

theorem inj (f : r ≼i s) {a b : α} : f a = f b ↔ a = b :=
  f.toRelEmbedding.inj

Injectivity of Initial Segment Embeddings

Informal description

For any initial segment embedding $f \colon r \preceq_i s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $a, b \in \alpha$, we have $f(a) = f(b)$ if and only if $a = b$.

InitialSeg.exists_eq_iff_rel theorem

(f : r ≼i s) {a : α} {b : β} : s b (f a) ↔ ∃ a', f a' = b ∧ r a' a

Full source

theorem exists_eq_iff_rel (f : r ≼i s) {a : α} {b : β} : s b (f a) ↔ ∃ a', f a' = b ∧ r a' a :=
  ⟨fun h => by
    rcases f.mem_range_of_rel h with ⟨a', rfl⟩
    exact ⟨a', rfl, f.map_rel_iff.1 h⟩,
    fun ⟨_, e, h⟩ => e ▸ f.map_rel_iff.2 h⟩

Characterization of Elements Below Initial Segment Embedding

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ a relation on a type $\beta$. For any initial segment embedding $f \colon r \preceq_i s$, element $a \in \alpha$, and element $b \in \beta$, we have $b \mathrel{s} f(a)$ if and only if there exists $a' \in \alpha$ such that $f(a') = b$ and $a' \mathrel{r} a$.

RelIso.toInitialSeg definition

(f : r ≃r s) : r ≼i s

Full source

/-- A relation isomorphism is an initial segment embedding -/
@[simps!]
def _root_.RelIso.toInitialSeg (f : r ≃r s) : r ≼i s :=
  ⟨f, by simp⟩

Relation isomorphism to initial segment embedding conversion

Informal description

Given a relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, the function converts $f$ into an initial segment embedding $f : r \preceq_i s$ by preserving the relation mapping property and ensuring the range forms a lower set.

InitialSeg.refl definition

(r : α → α → Prop) : r ≼i r

Full source

/-- The identity function shows that `≼i` is reflexive -/
@[refl]
protected def refl (r : α → α → Prop) : r ≼i r :=
  (RelIso.refl r).toInitialSeg

Reflexivity of initial segment embeddings

Informal description

The identity function on a type $\alpha$ with a relation $r$ is an initial segment embedding from $r$ to itself. That is, the identity function preserves the relation $r$ and its range forms a lower set, meaning for any elements $a, b \in \alpha$, if $b < a$ under $r$, then $b$ is in the range of the identity function (which it always is).

InitialSeg.instInhabited instance

(r : α → α → Prop) : Inhabited (r ≼i r)

Full source

instance (r : α → α → Prop) : Inhabited (r ≼i r) :=
  ⟨InitialSeg.refl r⟩

Inhabited Initial Segment Embeddings

Informal description

For any relation $r$ on a type $\alpha$, the type of initial segment embeddings $r \preceq_i r$ is inhabited.

InitialSeg.trans definition

(f : r ≼i s) (g : s ≼i t) : r ≼i t

Full source

/-- Composition of functions shows that `≼i` is transitive -/
@[trans]
protected def trans (f : r ≼i s) (g : s ≼i t) : r ≼i t :=
  ⟨f.1.trans g.1, fun a c h => by
    simp only [RelEmbedding.coe_trans, coe_coe_fn, comp_apply] at h ⊢
    rcases g.2 _ _ h with ⟨b, rfl⟩; have h := g.map_rel_iff.1 h
    rcases f.2 _ _ h with ⟨a', rfl⟩; exact ⟨a', rfl⟩⟩

Transitivity of initial segment embeddings

Informal description

Given two initial segment embeddings $f : r \preceq_i s$ and $g : s \preceq_i t$, their composition $g \circ f$ is an initial segment embedding from $r$ to $t$. This means that the composition preserves the order and the image of $g \circ f$ forms a lower set in $t$.

InitialSeg.refl_apply theorem

(x : α) : InitialSeg.refl r x = x

Full source

@[simp]
theorem refl_apply (x : α) : InitialSeg.refl r x = x :=
  rfl

Reflexive Initial Segment Embedding Acts as Identity

Informal description

For any element $x$ of a type $\alpha$ with a relation $r$, the reflexive initial segment embedding $\text{refl}_r$ applied to $x$ is equal to $x$ itself, i.e., $\text{refl}_r(x) = x$.

InitialSeg.trans_apply theorem

(f : r ≼i s) (g : s ≼i t) (a : α) : (f.trans g) a = g (f a)

Full source

@[simp]
theorem trans_apply (f : r ≼i s) (g : s ≼i t) (a : α) : (f.trans g) a = g (f a) :=
  rfl

Composition of Initial Segment Embeddings Preserves Application

Informal description

Let $r$, $s$, and $t$ be relations on types $\alpha$, $\beta$, and $\gamma$ respectively. Given initial segment embeddings $f : r \preceq_i s$ and $g : s \preceq_i t$, the composition $f \circ g$ satisfies $(f \circ g)(a) = g(f(a))$ for any $a \in \alpha$.

InitialSeg.subsingleton_of_trichotomous_of_irrefl instance

[IsTrichotomous β s] [IsIrrefl β s] [IsWellFounded α r] : Subsingleton (r ≼i s)

Full source

instance subsingleton_of_trichotomous_of_irrefl [IsTrichotomous β s] [IsIrrefl β s]
    [IsWellFounded α r] : Subsingleton (r ≼i s) where
  allEq f g := by
    ext a
    refine IsWellFounded.induction r a fun b IH =>
      extensional_of_trichotomous_of_irrefl s fun x => ?_
    rw [f.exists_eq_iff_rel, g.exists_eq_iff_rel]
    exact exists_congr fun x => and_congr_left fun hx => IH _ hx ▸ Iff.rfl

Uniqueness of Initial Segment Embeddings for Trichotomous and Irreflexive Relations

Informal description

For any relations $r$ on $\alpha$ and $s$ on $\beta$, if $s$ is trichotomous and irreflexive, and $r$ is well-founded, then the type of initial segment embeddings $r \preceq_i s$ is a subsingleton (i.e., has at most one element).

InitialSeg.instSubsingletonOfIsWellOrder instance

[IsWellOrder β s] : Subsingleton (r ≼i s)

Full source

/-- Given a well order `s`, there is at most one initial segment embedding of `r` into `s`. -/
instance [IsWellOrder β s] : Subsingleton (r ≼i s) :=
  ⟨fun a => have := a.isWellFounded; Subsingleton.elim a⟩

Uniqueness of Initial Segment Embeddings for Well-Orders

Informal description

For any well-order $s$ on a type $\beta$, there is at most one initial segment embedding from a relation $r$ on $\alpha$ to $s$.

InitialSeg.eq theorem

[IsWellOrder β s] (f g : r ≼i s) (a) : f a = g a

Full source

protected theorem eq [IsWellOrder β s] (f g : r ≼i s) (a) : f a = g a := by
  rw [Subsingleton.elim f g]

Uniqueness of Initial Segment Embeddings on Well-Orders

Informal description

Let $r$ be a relation on a type $\alpha$ and $s$ be a well-order on a type $\beta$. For any two initial segment embeddings $f, g : r \preceq_i s$ and any element $a \in \alpha$, we have $f(a) = g(a)$.

InitialSeg.antisymm definition

[IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) : r ≃r s

Full source

/-- If we have order embeddings between `α` and `β` whose ranges are initial segments, and `β` is a
well order, then `α` and `β` are order-isomorphic. -/
def antisymm [IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) : r ≃r s :=
  have := f.toRelEmbedding.isWellOrder
  ⟨⟨f, g, antisymm_aux f g, antisymm_aux g f⟩, f.map_rel_iff'⟩

Antisymmetry of initial segment embeddings for well-orders

Informal description

Given two well-orders $r$ on $\alpha$ and $s$ on $\beta$, if there exist initial segment embeddings $f : r \preceq_i s$ and $g : s \preceq_i r$, then $r$ and $s$ are order-isomorphic.

InitialSeg.antisymm_toFun theorem

[IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) : (antisymm f g : α → β) = f

Full source

@[simp]
theorem antisymm_toFun [IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) : (antisymm f g : α → β) = f :=
  rfl

Underlying Function of Antisymmetry Isomorphism Equals First Embedding

Informal description

Let $r$ and $s$ be well-orders on types $\alpha$ and $\beta$ respectively. Given initial segment embeddings $f : r \preceq_i s$ and $g : s \preceq_i r$, the underlying function of the order isomorphism $\text{antisymm}\,f\,g$ equals $f$.

InitialSeg.antisymm_symm theorem

[IsWellOrder α r] [IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) : (antisymm f g).symm = antisymm g f

Full source

@[simp]
theorem antisymm_symm [IsWellOrder α r] [IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) :
    (antisymm f g).symm = antisymm g f :=
  RelIso.coe_fn_injective rfl

Inverse of Antisymmetry Isomorphism for Initial Segments

Informal description

Let $r$ and $s$ be well-orders on types $\alpha$ and $\beta$ respectively. Given initial segment embeddings $f : r \preceq_i s$ and $g : s \preceq_i r$, the inverse of the order isomorphism $\text{antisymm}\,f\,g$ equals $\text{antisymm}\,g\,f$.

InitialSeg.codRestrict definition

(p : Set β) (f : r ≼i s) (H : ∀ a, f a ∈ p) : r ≼i Subrel s (· ∈ p)

Full source

/-- Restrict the codomain of an initial segment -/
def codRestrict (p : Set β) (f : r ≼i s) (H : ∀ a, f a ∈ p) : r ≼i Subrel s (· ∈ p) :=
  ⟨RelEmbedding.codRestrict p f H, fun a ⟨b, m⟩ h =>
    let ⟨a', e⟩ := f.mem_range_of_rel h
    ⟨a', by subst e; rfl⟩⟩

Codomain restriction of an initial segment embedding

Informal description

Given a subset $p$ of $\beta$, an initial segment embedding $f : r \preceq_i s$ from relation $r$ on $\alpha$ to relation $s$ on $\beta$, and a proof $H$ that for every $a \in \alpha$, $f(a) \in p$, the function constructs an initial segment embedding from $r$ to the restriction of $s$ to the subset $p$. In other words, this operation restricts the codomain of the initial segment embedding $f$ to the subset $p$ while preserving the initial segment property.

InitialSeg.codRestrict_apply theorem

(p) (f : r ≼i s) (H a) : codRestrict p f H a = ⟨f a, H a⟩

Full source

@[simp]
theorem codRestrict_apply (p) (f : r ≼i s) (H a) : codRestrict p f H a = ⟨f a, H a⟩ :=
  rfl

Codomain-Restricted Initial Segment Embedding Application

Informal description

Given a subset $p$ of $\beta$, an initial segment embedding $f : r \preceq_i s$, and a proof $H$ that for every $a \in \alpha$, $f(a) \in p$, the application of the codomain-restricted embedding $\text{codRestrict}\ p\ f\ H$ to an element $a \in \alpha$ yields the pair $\langle f(a), H(a) \rangle$.

InitialSeg.ofIsEmpty definition

(r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] : r ≼i s

Full source

/-- Initial segment embedding from an empty type. -/
def ofIsEmpty (r : α → α → Prop) (s : β → β → Prop) [IsEmpty α] : r ≼i s :=
  ⟨RelEmbedding.ofIsEmpty r s, isEmptyElim⟩

Initial segment embedding from an empty type

Informal description

Given relations $r$ on an empty type $\alpha$ and $s$ on any type $\beta$, there exists an initial segment embedding from $r$ to $s$. This is constructed using the unique embedding from an empty type, where all statements about elements of $\alpha$ are vacuously true, and the range of this embedding is trivially an initial segment since $\alpha$ has no elements.

InitialSeg.leAdd definition

(r : α → α → Prop) (s : β → β → Prop) : r ≼i Sum.Lex r s

Full source

/-- Initial segment embedding of an order `r` into the disjoint union of `r` and `s`. -/
def leAdd (r : α → α → Prop) (s : β → β → Prop) : r ≼i Sum.Lex r s :=
  ⟨⟨⟨Sum.inl, fun _ _ => Sum.inl.inj⟩, Sum.lex_inl_inl⟩, fun a b => by
    cases b <;> [exact fun _ => ⟨_, rfl⟩; exact False.elim ∘ Sum.lex_inr_inl]⟩

Initial segment embedding into lexicographic sum

Informal description

For any relations $r$ on $\alpha$ and $s$ on $\beta$, there exists an initial segment embedding from $r$ to the lexicographic sum of $r$ and $s$. This embedding maps each element $a \in \alpha$ to $\text{inl}(a) \in \alpha \oplus \beta$, where $\text{inl}$ is the left inclusion map. The range of this embedding consists precisely of the elements of the form $\text{inl}(a)$, which forms an initial segment in the lexicographic order on $\alpha \oplus \beta$.

InitialSeg.leAdd_apply theorem

(r : α → α → Prop) (s : β → β → Prop) (a) : leAdd r s a = Sum.inl a

Full source

@[simp]
theorem leAdd_apply (r : α → α → Prop) (s : β → β → Prop) (a) : leAdd r s a = Sum.inl a :=
  rfl

Application of Initial Segment Embedding to Lexicographic Sum

Informal description

For any relations $r$ on $\alpha$ and $s$ on $\beta$, the initial segment embedding $\text{leAdd}\ r\ s$ maps an element $a \in \alpha$ to the left inclusion $\text{inl}(a) \in \alpha \oplus \beta$.

InitialSeg.acc theorem

(f : r ≼i s) (a : α) : Acc r a ↔ Acc s (f a)

Full source

protected theorem acc (f : r ≼i s) (a : α) : AccAcc r a ↔ Acc s (f a) :=
  ⟨by
    refine fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => ?_
    obtain ⟨a', rfl⟩ := f.mem_range_of_rel hb
    exact ha _ (f.map_rel_iff.mp hb), f.toRelEmbedding.acc a⟩

Accessibility Preservation under Initial Segment Embeddings

Informal description

Let $r$ be a relation on $\alpha$ and $s$ a relation on $\beta$. For any initial segment embedding $f \colon r \preceq_i s$ and any element $a \in \alpha$, the element $a$ is accessible with respect to $r$ if and only if $f(a)$ is accessible with respect to $s$. Here, an element $x$ is called *accessible* with respect to a relation $R$ if every descending $R$-chain starting from $x$ is finite.

PrincipalSeg structure

{α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends r ↪r s

Full source

/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≺i s` is an initial
segment embedding whose range is `Set.Iio x` for some element `x`. If `β` is a well order, this is
equivalent to the embedding not being surjective. -/
structure PrincipalSeg {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends r ↪r s where
  /-- The supremum of the principal segment -/
  top : β
  /-- The range of the order embedding is the set of elements `b` such that `s b top` -/
  mem_range_iff_rel' : ∀ b, b ∈ Set.range toRelEmbeddingb ∈ Set.range toRelEmbedding ↔ s b top

Principal segment embedding

Informal description

A principal segment embedding between two relations `r` on `α` and `s` on `β` is an order embedding `f : r ↪r s` whose range is the set of all elements strictly below some fixed element `x` in `β` (i.e., the range is `Set.Iio x`). If `β` is well-ordered, this is equivalent to `f` not being surjective.

InitialSeg.term_≺i_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped[InitialSeg] infixl:25 " ≺i " => PrincipalSeg

Notation for principal segment embeddings

Informal description

The notation `r ≺i s` represents the type of principal segment embeddings from relation `r` to relation `s`, where a principal segment embedding is an order embedding whose range forms a principal segment (a set of the form `{y | y < x}` for some `x`).

term_
      definition


    
      
         : Lean.TrailingParserDescr✝
        
          Full source
          /-- A `PrincipalSeg` between the `<` relations of two types. -/
notation:25 α:24 " <i " β:25 => @PrincipalSeg α β (· < ·) (· < ·)
        
      

      
        Principal segment embedding between strict orders
        
          Informal description
          The notation `α


        
          
    
      PrincipalSeg.instCoeOutRelEmbedding
      instance
    
    
      
         : CoeOut (r ≺i s) (r ↪r s)
        
          Full source
          instance : CoeOut (r ≺i s) (r ↪r s) :=
  ⟨PrincipalSeg.toRelEmbedding⟩
        
      

      
        Principal Segments as Relation Embeddings
        
          Informal description
          Every principal segment embedding $r \prec_i s$ can be viewed as a relation embedding $r \hookrightarrow_r s$.
        
      
    
  
        
          
    
      PrincipalSeg.instCoeFunForall
      instance
    
    
      
         : CoeFun (r ≺i s) fun _ => α → β
        
          Full source
          instance : CoeFun (r ≺i s) fun _ => α → β :=
  ⟨fun f => f⟩
        
      

      
        Principal Segment Embeddings as Functions
        
          Informal description
          Every principal segment embedding $r \prec_i s$ can be coerced to a function from $\alpha$ to $\beta$.
        
      
    
  
        
          
    
      PrincipalSeg.toRelEmbedding_injective
      theorem
    
    
      
         [IsIrrefl β s] [IsTrichotomous β s] : Function.Injective (@toRelEmbedding α β r s)
        
          Full source
          theorem toRelEmbedding_injective [IsIrrefl β s] [IsTrichotomous β s] :
    Function.Injective (@toRelEmbedding α β r s) := by
  rintro ⟨f, a, hf⟩ ⟨g, b, hg⟩ rfl
  congr
  refine extensional_of_trichotomous_of_irrefl s fun x ↦ ?_
  rw [← hf, hg]
        
      

      
        Injectivity of Principal Segment Embeddings as Relation Embeddings
        
          Informal description
          Let $\alpha$ and $\beta$ be types equipped with relations $r$ and $s$ respectively, where $s$ is irreflexive and trichotomous on $\beta$. Then the function mapping a principal segment embedding $f : r \prec_i s$ to its underlying relation embedding $f : r \hookrightarrow_r s$ is injective.
        
      
    
  
        
          
    
      PrincipalSeg.toRelEmbedding_inj
      theorem
    
    
      
         [IsIrrefl β s] [IsTrichotomous β s] {f g : r ≺i s} : f.toRelEmbedding = g.toRelEmbedding ↔ f = g
        
          Full source
          @[simp]
theorem toRelEmbedding_inj [IsIrrefl β s] [IsTrichotomous β s] {f g : r ≺i s} :
    f.toRelEmbedding = g.toRelEmbedding ↔ f = g :=
  toRelEmbedding_injective.eq_iff
        
      

      
        Equality of Principal Segment Embeddings via Underlying Relation Embeddings
        
          Informal description
          Let $\alpha$ and $\beta$ be types equipped with irreflexive and trichotomous relations $r$ and $s$ respectively. For any two principal segment embeddings $f, g : r \prec_i s$, the underlying relation embeddings $f$ and $g$ are equal if and only if $f$ and $g$ are equal as principal segment embeddings.
        
      
    
  
        
          
    
      PrincipalSeg.ext
      theorem
    
    
      
         [IsIrrefl β s] [IsTrichotomous β s] {f g : r ≺i s} (h : ∀ x, f x = g x) : f = g
        
          Full source
          @[ext]
theorem ext [IsIrrefl β s] [IsTrichotomous β s] {f g : r ≺i s} (h : ∀ x, f x = g x) : f = g := by
  rw [← toRelEmbedding_inj]
  ext
  exact h _
        
      

      
        Extensionality of Principal Segment Embeddings
        
          Informal description
          Let $r$ and $s$ be irreflexive and trichotomous relations on types $\alpha$ and $\beta$ respectively. For any two principal segment embeddings $f, g : r \prec_i s$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.
        
      
    
  
        
          
    
      PrincipalSeg.coe_fn_mk
      theorem
    
    
      
         (f : r ↪r s) (t o) : (@PrincipalSeg.mk _ _ r s f t o : α → β) = f
        
          Full source
          @[simp]
theorem coe_fn_mk (f : r ↪r s) (t o) : (@PrincipalSeg.mk _ _ r s f t o : α → β) = f :=
  rfl
        
      

      
        Principal Segment Embedding Construction Preserves Underlying Function
        
          Informal description
          For any relation embedding $f : r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any top element $t$ and proof $o$ that $t$ is not in the range of $f$, the function associated with the principal segment embedding constructed from $f$, $t$, and $o$ is equal to $f$ itself.
        
      
    
  
        
          
    
      PrincipalSeg.mem_range_iff_rel
      theorem
    
    
      
         (f : r ≺i s) : ∀ {b : β}, b ∈ Set.range f ↔ s b f.top
        
          Full source
          theorem mem_range_iff_rel (f : r ≺i s) : ∀ {b : β}, b ∈ Set.range fb ∈ Set.range f ↔ s b f.top :=
  f.mem_range_iff_rel' _
        
      

      
        Characterization of Elements in the Range of a Principal Segment Embedding
        
          Informal description
          For any principal segment embedding $f : r \prec_i s$ and any element $b \in \beta$, $b$ belongs to the range of $f$ if and only if $b$ is related to the top element $f.\text{top}$ under the relation $s$, i.e., $b \in \text{range}(f) \leftrightarrow s(b, f.\text{top})$.
        
      
    
  
        
          
    
      PrincipalSeg.lt_top
      theorem
    
    
      
         (f : r ≺i s) (a : α) : s (f a) f.top
        
          Full source
          theorem lt_top (f : r ≺i s) (a : α) : s (f a) f.top :=
  f.mem_range_iff_rel.1 ⟨_, rfl⟩
        
      

      
        Image under Principal Segment Embedding is Below Top Element
        
          Informal description
          For any principal segment embedding $f : r \prec_i s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any element $a \in \alpha$, the image $f(a)$ is related to the top element $f.\text{top}$ under the relation $s$, i.e., $s(f(a), f.\text{top})$ holds.
        
      
    
  
        
          
    
      PrincipalSeg.mem_range_of_rel_top
      theorem
    
    
      
         (f : r ≺i s) {b : β} (h : s b f.top) : b ∈ Set.range f
        
          Full source
          theorem mem_range_of_rel_top (f : r ≺i s) {b : β} (h : s b f.top) : b ∈ Set.range f :=
  f.mem_range_iff_rel.2 h
        
      

      
        Elements Below Top in Principal Segment Embedding Belong to Range
        
          Informal description
          For any principal segment embedding $f : r \prec_i s$ and any element $b \in \beta$, if $b$ is related to the top element $f.\text{top}$ under the relation $s$ (i.e., $s(b, f.\text{top})$ holds), then $b$ belongs to the range of $f$.
        
      
    
  
        
          
    
      PrincipalSeg.mem_range_of_rel
      theorem
    
    
      
         [IsTrans β s] (f : r ≺i s) {a : α} {b : β} (h : s b (f a)) : b ∈ Set.range f
        
          Full source
          theorem mem_range_of_rel [IsTrans β s] (f : r ≺i s) {a : α} {b : β} (h : s b (f a)) :
    b ∈ Set.range f :=
  f.mem_range_of_rel_top <| _root_.trans h <| f.lt_top _
        
      

      
        Elements Below Images in Principal Segment Embedding Belong to Range
        
          Informal description
          Let $r$ and $s$ be relations on types $\alpha$ and $\beta$ respectively, with $s$ being transitive. For any principal segment embedding $f : r \prec_i s$, if $b \in \beta$ is related to some image $f(a) \in \beta$ under $s$ (i.e., $s(b, f(a))$ holds), then $b$ belongs to the range of $f$.
        
      
    
  
        
          
    
      PrincipalSeg.surjOn
      theorem
    
    
      
         (f : r ≺i s) : Set.SurjOn f Set.univ {b | s b f.top}
        
          Full source
          theorem surjOn (f : r ≺i s) : Set.SurjOn f Set.univ { b | s b f.top } := by
  intro b h
  simpa using mem_range_of_rel_top _ h
        
      

      
        Surjectivity of Principal Segment Embedding onto Elements Below Top
        
          Informal description
          For any principal segment embedding $f : r \prec_i s$, the function $f$ is surjective from the universal set $\text{univ}$ to the set $\{b \mid s(b, f.\text{top})\}$ of all elements in $\beta$ that are related to the top element $f.\text{top}$ under the relation $s$.
        
      
    
  
        
          
    
      PrincipalSeg.hasCoeInitialSeg
      instance
    
    
      
         [IsTrans β s] : Coe (r ≺i s) (r ≼i s)
        
          Full source
          /-- A principal segment embedding is in particular an initial segment embedding. -/
instance hasCoeInitialSeg [IsTrans β s] : Coe (r ≺i s) (r ≼i s) :=
  ⟨fun f => ⟨f.toRelEmbedding, fun _ _ => f.mem_range_of_rel⟩⟩
        
      

      
        Principal Segment Embeddings as Initial Segment Embeddings
        
          Informal description
          For any transitive relation $s$ on a type $\beta$, every principal segment embedding $f : r \prec_i s$ can be viewed as an initial segment embedding $f : r \preccurlyeq_i s$. This means that the embedding $f$ preserves the order structure and its range forms a lower set in $\beta$.
        
      
    
  
        
          
    
      PrincipalSeg.coe_coe_fn'
      theorem
    
    
      
         [IsTrans β s] (f : r ≺i s) : ((f : r ≼i s) : α → β) = f
        
          Full source
          theorem coe_coe_fn' [IsTrans β s] (f : r ≺i s) : ((f : r ≼i s) : α → β) = f :=
  rfl
        
      

      
        Coercion of Principal Segment to Initial Segment Preserves Underlying Function
        
          Informal description
          Let $r$ and $s$ be relations on types $\alpha$ and $\beta$ respectively, with $s$ being transitive. For any principal segment embedding $f : r \prec_i s$, the underlying function of $f$ when viewed as an initial segment embedding (via coercion) is equal to $f$ itself as a function from $\alpha$ to $\beta$.

In other words, if we coerce a principal segment embedding $f$ to an initial segment embedding and then to a function, we get the same function as $f$ itself.
        
      
    
  
        
          
    
      PrincipalSeg.exists_eq_iff_rel
      theorem
    
    
      
         [IsTrans β s] (f : r ≺i s) {a : α} {b : β} : s b (f a) ↔ ∃ a', f a' = b ∧ r a' a
        
          Full source
          theorem exists_eq_iff_rel [IsTrans β s] (f : r ≺i s) {a : α} {b : β} :
    s b (f a) ↔ ∃ a', f a' = b ∧ r a' a :=
  @InitialSeg.exists_eq_iff_rel α β r s f a b
        
      

      
        Characterization of Elements Below Principal Segment Embedding
        
          Informal description
          Let $r$ be a relation on a type $\alpha$ and $s$ a transitive relation on a type $\beta$. For any principal segment embedding $f \colon r \prec_i s$, element $a \in \alpha$, and element $b \in \beta$, we have $b \mathrel{s} f(a)$ if and only if there exists $a' \in \alpha$ such that $f(a') = b$ and $a' \mathrel{r} a$.
        
      
    
  
        
          
    
      InitialSeg.toPrincipalSeg
      definition
    
    
      
         [IsWellOrder β s] (f : r ≼i s) (hf : ¬Surjective f) : r ≺i s
        
          Full source
          /-- A principal segment is the same as a non-surjective initial segment. -/
noncomputable def _root_.InitialSeg.toPrincipalSeg [IsWellOrder β s] (f : r ≼i s)
    (hf : ¬ Surjective f) : r ≺i s :=
  ⟨f, _, Classical.choose_spec (f.eq_or_principal.resolve_left hf)⟩
        
      

      
        Conversion from non-surjective initial segment to principal segment
        
          Informal description
          Given a well-order $s$ on $\beta$ and an initial segment embedding $f : r \preceq_i s$ that is not surjective, this constructs a principal segment embedding $r \prec_i s$. The embedding $f$ remains unchanged, but its range is now recognized as a principal segment (a set of the form $\{y \mid y < x\}$ for some $x \in \beta$).
        
      
    
  
        
          
    
      InitialSeg.toPrincipalSeg_apply
      theorem
    
    
      
         [IsWellOrder β s] (f : r ≼i s) (hf : ¬Surjective f) (x : α) : f.toPrincipalSeg hf x = f x
        
          Full source
          @[simp]
theorem _root_.InitialSeg.toPrincipalSeg_apply [IsWellOrder β s] (f : r ≼i s)
    (hf : ¬ Surjective f) (x : α) : f.toPrincipalSeg hf x = f x :=
  rfl
        
      

      
        Equality of Initial and Principal Segment Embeddings on Elements
        
          Informal description
          Given a well-order $s$ on $\beta$ and an initial segment embedding $f : r \preceq_i s$ that is not surjective, the principal segment embedding $f.\text{toPrincipalSeg} \, hf$ constructed from $f$ satisfies $(f.\text{toPrincipalSeg} \, hf)(x) = f(x)$ for all $x \in \alpha$.
        
      
    
  
        
          
    
      PrincipalSeg.irrefl
      theorem
    
    
      
         {r : α → α → Prop} [IsWellOrder α r] (f : r ≺i r) : False
        
          Full source
          theorem irrefl {r : α → α → Prop} [IsWellOrder α r] (f : r ≺i r) : False := by
  have h := f.lt_top f.top
  rw [show f f.top = f.top from InitialSeg.eq f (InitialSeg.refl r) f.top] at h
  exact _root_.irrefl _ h
        
      

      
        Irreflexivity of Principal Segment Embeddings on Well-Orders
        
          Informal description
          For any well-order $r$ on a type $\alpha$, there does not exist a principal segment embedding from $r$ to itself. In other words, the type of principal segment embeddings $r \prec_i r$ is empty.
        
      
    
  
        
          
    
      PrincipalSeg.instIsEmptyOfIsWellOrder
      instance
    
    
      
         (r : α → α → Prop) [IsWellOrder α r] : IsEmpty (r ≺i r)
        
          Full source
          instance (r : α → α → Prop) [IsWellOrder α r] : IsEmpty (r ≺i r) :=
  ⟨fun f => f.irrefl⟩
        
      

      
        No Principal Segment Embedding from a Well-Order to Itself
        
          Informal description
          For any well-order $r$ on a type $\alpha$, the type of principal segment embeddings from $r$ to itself is empty.
        
      
    
  
        
          
    
      PrincipalSeg.transInitial
      definition
    
    
      
         (f : r ≺i s) (g : s ≼i t) : r ≺i t
        
          Full source
          /-- Composition of a principal segment embedding with an initial segment embedding, as a principal
segment embedding -/
def transInitial (f : r ≺i s) (g : s ≼i t) : r ≺i t :=
  ⟨@RelEmbedding.trans _ _ _ r s t f g, g f.top, fun a => by
    simp [g.exists_eq_iff_rel, ← PrincipalSeg.mem_range_iff_rel, exists_swap, ← exists_and_left]⟩
        
      

      
        Composition of principal and initial segment embeddings
        
          Informal description
          Given a principal segment embedding $f : r \prec_i s$ and an initial segment embedding $g : s \preceq_i t$, their composition $g \circ f$ forms a principal segment embedding from $r$ to $t$. The top element of the resulting principal segment is the image under $g$ of the top element of $f$.
        
      
    
  
        
          
    
      PrincipalSeg.transInitial_apply
      theorem
    
    
      
         (f : r ≺i s) (g : s ≼i t) (a : α) : f.transInitial g a = g (f a)
        
          Full source
          @[simp]
theorem transInitial_apply (f : r ≺i s) (g : s ≼i t) (a : α) : f.transInitial g a = g (f a) :=
  rfl
        
      

      
        Composition Formula for Principal and Initial Segment Embeddings
        
          Informal description
          Let $r$, $s$, and $t$ be relations on types $\alpha$, $\beta$, and $\gamma$ respectively. Given a principal segment embedding $f : r \prec_i s$ and an initial segment embedding $g : s \preceq_i t$, the composition $g \circ f$ (denoted $f.\text{transInitial}\ g$) satisfies $(g \circ f)(a) = g(f(a))$ for all $a \in \alpha$.
        
      
    
  
        
          
    
      PrincipalSeg.transInitial_top
      theorem
    
    
      
         (f : r ≺i s) (g : s ≼i t) : (f.transInitial g).top = g f.top
        
          Full source
          @[simp]
theorem transInitial_top (f : r ≺i s) (g : s ≼i t) : (f.transInitial g).top = g f.top :=
  rfl
        
      

      
        Top Element Preservation in Composition of Principal and Initial Segment Embeddings
        
          Informal description
          Let $f : r \prec_i s$ be a principal segment embedding and $g : s \preceq_i t$ be an initial segment embedding. Then the top element of the composed principal segment embedding $f \circ g$ is equal to $g$ applied to the top element of $f$, i.e., $(f \circ g).\text{top} = g(f.\text{top})$.
        
      
    
  
        
          
    
      PrincipalSeg.trans
      definition
    
    
      
         [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) : r ≺i t
        
          Full source
          /-- Composition of two principal segment embeddings as a principal segment embedding -/
@[trans]
protected def trans [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) : r ≺i t :=
  transInitial f g
        
      

      
        Composition of principal segment embeddings
        
          Informal description
          Given transitive relations $r$ on $\alpha$, $s$ on $\beta$, and $t$ on $\gamma$, the composition of two principal segment embeddings $f : r \prec_i s$ and $g : s \prec_i t$ forms a principal segment embedding from $r$ to $t$. The top element of the resulting principal segment is the image under $g$ of the top element of $f$.
        
      
    
  
        
          
    
      PrincipalSeg.trans_apply
      theorem
    
    
      
         [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) (a : α) : f.trans g a = g (f a)
        
          Full source
          @[simp]
theorem trans_apply [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) (a : α) : f.trans g a = g (f a) :=
  rfl
        
      

      
        Composition Formula for Principal Segment Embeddings: $(f \circ g)(a) = g(f(a))$
        
          Informal description
          Given transitive relations $r$ on $\alpha$, $s$ on $\beta$, and $t$ on $\gamma$, and principal segment embeddings $f : r \prec_i s$ and $g : s \prec_i t$, the composition $f \circ g$ evaluated at any element $a \in \alpha$ satisfies $(f \circ g)(a) = g(f(a))$.
        
      
    
  
        
          
    
      PrincipalSeg.trans_top
      theorem
    
    
      
         [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) : (f.trans g).top = g f.top
        
          Full source
          @[simp]
theorem trans_top [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) : (f.trans g).top = g f.top :=
  rfl
        
      

      
        Top Element Preservation under Composition of Principal Segment Embeddings
        
          Informal description
          Given transitive relations $r$ on $\alpha$, $s$ on $\beta$, and $t$ on $\gamma$, and principal segment embeddings $f : r \prec_i s$ and $g : s \prec_i t$, the top element of the composed principal segment embedding $f \circ g$ is equal to $g$ applied to the top element of $f$, i.e., $(f \circ g).\text{top} = g(f.\text{top})$.
        
      
    
  
        
          
    
      PrincipalSeg.relIsoTrans
      definition
    
    
      
         (f : r ≃r s) (g : s ≺i t) : r ≺i t
        
          Full source
          /-- Composition of an order isomorphism with a principal segment embedding, as a principal
segment embedding -/
def relIsoTrans (f : r ≃r s) (g : s ≺i t) : r ≺i t :=
  ⟨@RelEmbedding.trans _ _ _ r s t f g, g.top, fun c => by simp [g.mem_range_iff_rel]⟩
        
      

      
        Composition of relation isomorphism with principal segment embedding
        
          Informal description
          Given a relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and a principal segment embedding $g : s \prec t$ from $s$ to a relation $t$ on $\gamma$, the composition $g \circ f$ forms a principal segment embedding from $r$ to $t$. The top element of the resulting principal segment is the same as the top element of $g$.
        
      
    
  
        
          
    
      PrincipalSeg.relIsoTrans_apply
      theorem
    
    
      
         (f : r ≃r s) (g : s ≺i t) (a : α) : relIsoTrans f g a = g (f a)
        
          Full source
          @[simp]
theorem relIsoTrans_apply (f : r ≃r s) (g : s ≺i t) (a : α) : relIsoTrans f g a = g (f a) :=
  rfl
        
      

      
        Application of Composition of Relation Isomorphism with Principal Segment Embedding
        
          Informal description
          Given a relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and a principal segment embedding $g : s \prec t$ from $s$ to a relation $t$ on $\gamma$, the composition $g \circ f$ evaluated at any element $a \in \alpha$ satisfies $(g \circ f)(a) = g(f(a))$.
        
      
    
  
        
          
    
      PrincipalSeg.relIsoTrans_top
      theorem
    
    
      
         (f : r ≃r s) (g : s ≺i t) : (relIsoTrans f g).top = g.top
        
          Full source
          @[simp]
theorem relIsoTrans_top (f : r ≃r s) (g : s ≺i t) : (relIsoTrans f g).top = g.top :=
  rfl
        
      

      
        Top Element Preservation in Composition of Relation Isomorphism with Principal Segment Embedding
        
          Informal description
          Given a relation isomorphism $f : r \simeq s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and a principal segment embedding $g : s \prec t$ from $s$ to a relation $t$ on $\gamma$, the top element of the composed principal segment embedding $g \circ f$ is equal to the top element of $g$.
        
      
    
  
        
          
    
      PrincipalSeg.transRelIso
      definition
    
    
      
         (f : r ≺i s) (g : s ≃r t) : r ≺i t
        
          Full source
          /-- Composition of a principal segment embedding with a relation isomorphism, as a principal segment
embedding -/
def transRelIso (f : r ≺i s) (g : s ≃r t) : r ≺i t :=
  transInitial f g.toInitialSeg
        
      

      
        Composition of principal segment embedding with relation isomorphism
        
          Informal description
          Given a principal segment embedding \( f : r \prec_i s \) and a relation isomorphism \( g : s \simeq_r t \), their composition \( g \circ f \) forms a principal segment embedding from \( r \) to \( t \). The top element of the resulting principal segment is the image under \( g \) of the top element of \( f \).
        
      
    
  
        
          
    
      PrincipalSeg.transRelIso_apply
      theorem
    
    
      
         (f : r ≺i s) (g : s ≃r t) (a : α) : transRelIso f g a = g (f a)
        
          Full source
          @[simp]
theorem transRelIso_apply (f : r ≺i s) (g : s ≃r t) (a : α) : transRelIso f g a = g (f a) :=
  rfl
        
      

      
        Composition of Principal Segment Embedding with Relation Isomorphism Preserves Application
        
          Informal description
          Given a principal segment embedding $f : r \prec_i s$ and a relation isomorphism $g : s \simeq_r t$, the composition $g \circ f$ applied to any element $a \in \alpha$ equals $g(f(a))$.
        
      
    
  
        
          
    
      PrincipalSeg.transRelIso_top
      theorem
    
    
      
         (f : r ≺i s) (g : s ≃r t) : (transRelIso f g).top = g f.top
        
          Full source
          @[simp]
theorem transRelIso_top (f : r ≺i s) (g : s ≃r t) : (transRelIso f g).top = g f.top :=
  rfl
        
      

      
        Top Element Preservation under Composition of Principal Segment Embedding and Relation Isomorphism
        
          Informal description
          Given a principal segment embedding $f \colon r \prec_i s$ and a relation isomorphism $g \colon s \simeq_r t$, the top element of the composed principal segment embedding $\text{transRelIso}\, f\, g$ is equal to $g$ applied to the top element of $f$, i.e., $(\text{transRelIso}\, f\, g).\text{top} = g(f.\text{top})$.
        
      
    
  
        
          
    
      PrincipalSeg.instSubsingletonOfIsWellOrder
      instance
    
    
      
         [IsWellOrder β s] : Subsingleton (r ≺i s)
        
          Full source
          /-- Given a well order `s`, there is a most one principal segment embedding of `r` into `s`. -/
instance [IsWellOrder β s] : Subsingleton (r ≺i s) where
  allEq f g := ext ((f : r ≼i s).eq g)
        
      

      
        Uniqueness of Principal Segment Embeddings for Well-Orders
        
          Informal description
          For any well-order $s$ on a type $\beta$, there is at most one principal segment embedding from any relation $r$ on a type $\alpha$ into $s$.
        
      
    
  
        
          
    
      PrincipalSeg.eq
      theorem
    
    
      
         [IsWellOrder β s] (f g : r ≺i s) (a) : f a = g a
        
          Full source
          protected theorem eq [IsWellOrder β s] (f g : r ≺i s) (a) : f a = g a := by
  rw [Subsingleton.elim f g]
        
      

      
        Uniqueness of Principal Segment Embeddings on Elements for Well-Orders
        
          Informal description
          For any well-order $s$ on a type $\beta$, and any two principal segment embeddings $f, g \colon r \prec_i s$ from a relation $r$ on $\alpha$, the images of any element $a \in \alpha$ under $f$ and $g$ are equal, i.e., $f(a) = g(a)$.
        
      
    
  
        
          
    
      PrincipalSeg.top_eq
      theorem
    
    
      
         [IsWellOrder γ t] (e : r ≃r s) (f : r ≺i t) (g : s ≺i t) : f.top = g.top
        
          Full source
          theorem top_eq [IsWellOrder γ t] (e : r ≃r s) (f : r ≺i t) (g : s ≺i t) : f.top = g.top := by
  rw [Subsingleton.elim f (PrincipalSeg.relIsoTrans e g)]; rfl
        
      

      
        Equality of Top Elements in Principal Segment Embeddings via Relation Isomorphism
        
          Informal description
          Let $r$, $s$, and $t$ be relations on types $\alpha$, $\beta$, and $\gamma$ respectively, with $t$ being a well-order on $\gamma$. Given a relation isomorphism $e : r \simeqr s$ and principal segment embeddings $f : r \prec_i t$ and $g : s \prec_i t$, the top elements of $f$ and $g$ are equal, i.e., $f.\text{top} = g.\text{top}$.
        
      
    
  
        
          
    
      PrincipalSeg.top_rel_top
      theorem
    
    
      
         {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder γ t] (f : r ≺i s) (g : s ≺i t) (h : r ≺i t) :
  t h.top g.top
        
          Full source
          theorem top_rel_top {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder γ t]
    (f : r ≺i s) (g : s ≺i t) (h : r ≺i t) : t h.top g.top := by
  rw [Subsingleton.elim h (f.trans g)]
  apply PrincipalSeg.lt_top
        
      

      
        Top Element Relation in Composition of Principal Segments
        
          Informal description
          Let $r$, $s$, and $t$ be relations on types $\alpha$, $\beta$, and $\gamma$ respectively, with $t$ being a well-order on $\gamma$. Given principal segment embeddings $f : r \prec_i s$, $g : s \prec_i t$, and $h : r \prec_i t$, the top element of $h$ is related to the top element of $g$ under the relation $t$, i.e., $t(h.\text{top}, g.\text{top})$ holds.
        
      
    
  
        
          
    
      PrincipalSeg.ofElement
      definition
    
    
      
         {α : Type*} (r : α → α → Prop) (a : α) : Subrel r (r · a) ≺i r
        
          Full source
          /-- Any element of a well order yields a principal segment. -/
@[simps!]
def ofElement {α : Type*} (r : α → α → Prop) (a : α) : SubrelSubrel r (r · a) ≺i r :=
  ⟨Subrel.relEmbedding _ _, a, fun _ => ⟨fun ⟨⟨_, h⟩, rfl⟩ => h, fun h => ⟨⟨_, h⟩, rfl⟩⟩⟩
        
      

      
        Principal segment embedding from elements less than a given element
        
          Informal description
          Given a relation $r$ on a type $\alpha$ and an element $a \in \alpha$, the principal segment embedding $\text{Subrel}\ r\ (r \cdot a) \prec_i r$ is defined, where $\text{Subrel}\ r\ (r \cdot a)$ is the restriction of $r$ to the set of elements less than $a$ under $r$. The embedding maps each element $b$ in the restricted relation to its underlying element in $\alpha$, and the top element of this principal segment is $a$.
        
      
    
  
        
          
    
      PrincipalSeg.ofElement_apply
      theorem
    
    
      
         {α : Type*} (r : α → α → Prop) (a : α) (b) : ofElement r a b = b.1
        
          Full source
          @[simp]
theorem ofElement_apply {α : Type*} (r : α → α → Prop) (a : α) (b) : ofElement r a b = b.1 :=
  rfl
        
      

      
        Principal segment embedding application equals underlying element
        
          Informal description
          Let $r$ be a relation on a type $\alpha$, and let $a \in \alpha$. For any element $b$ in the principal segment defined by elements less than $a$ under $r$, the application of the principal segment embedding $\text{ofElement}\ r\ a$ to $b$ equals the underlying element $b.1$ in $\alpha$.

In symbols: $\text{ofElement}\ r\ a\ b = b.1$ where $b$ is an element of the subtype $\{x \in \alpha \mid r\ x\ a\}$.
        
      
    
  
        
          
    
      PrincipalSeg.subrelIso
      definition
    
    
      
         (f : r ≺i s) : Subrel s (s · f.top) ≃r r
        
          Full source
          /-- For any principal segment `r ≺i s`, there is a `Subrel` of `s` order isomorphic to `r`. -/
@[simps! symm_apply]
noncomputable def subrelIso (f : r ≺i s) : SubrelSubrel s (s · f.top) ≃r r :=
  RelIso.symm ⟨(Equiv.ofInjective f f.injective).trans
    (Equiv.setCongr (funext fun _ ↦ propext f.mem_range_iff_rel)), f.map_rel_iff⟩
        
      

      
        Order isomorphism between a principal segment and the original relation
        
          Informal description
          For any principal segment embedding \( f : r \prec_i s \) between relations \( r \) on \( \alpha \) and \( s \) on \( \beta \), there exists a relation isomorphism between the restriction of \( s \) to the set of elements strictly below \( f.\text{top} \) (i.e., \( \text{Subrel}\ s\ (s \cdot f.\text{top}) \)) and the original relation \( r \). 

In other words, the subset of \( \beta \) consisting of elements less than \( f.\text{top} \) under \( s \) is order-isomorphic to \( \alpha \) with the relation \( r \).
        
      
    
  
        
          
    
      PrincipalSeg.apply_subrelIso
      theorem
    
    
      
         (f : r ≺i s) (b : { b // s b f.top }) : f (f.subrelIso b) = b
        
          Full source
          @[simp]
theorem apply_subrelIso (f : r ≺i s) (b : {b // s b f.top}) : f (f.subrelIso b) = b :=
  Equiv.apply_ofInjective_symm f.injective _
        
      

      
        Principal Segment Embedding Preserves Subrel Isomorphism Application
        
          Informal description
          Let $f : r \prec_i s$ be a principal segment embedding between relations $r$ on $\alpha$ and $s$ on $\beta$. For any element $b$ in the subset $\{b \in \beta \mid s(b, f.\text{top})\}$ (i.e., elements strictly below $f.\text{top}$ under $s$), applying $f$ to the image of $b$ under the order isomorphism $f.\text{subrelIso}$ yields $b$ itself. In other words, $f(f.\text{subrelIso}(b)) = b$.
        
      
    
  
        
          
    
      PrincipalSeg.subrelIso_apply
      theorem
    
    
      
         (f : r ≺i s) (a : α) : f.subrelIso ⟨f a, f.lt_top a⟩ = a
        
          Full source
          @[simp]
theorem subrelIso_apply (f : r ≺i s) (a : α) : f.subrelIso ⟨f a, f.lt_top a⟩ = a :=
  Equiv.ofInjective_symm_apply f.injective _
        
      

      
        Inverse of Principal Segment Isomorphism Maps Image Back to Original Element
        
          Informal description
          For any principal segment embedding $f : r \prec_i s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, and for any element $a \in \alpha$, the order isomorphism $f.\text{subrelIso}$ maps the pair $\langle f(a), f.\text{lt\_top}(a) \rangle$ back to $a$.
        
      
    
  
        
          
    
      PrincipalSeg.codRestrict
      definition
    
    
      
         (p : Set β) (f : r ≺i s) (H : ∀ a, f a ∈ p) (H₂ : f.top ∈ p) : r ≺i Subrel s (· ∈ p)
        
          Full source
          /-- Restrict the codomain of a principal segment embedding. -/
def codRestrict (p : Set β) (f : r ≺i s) (H : ∀ a, f a ∈ p) (H₂ : f.top ∈ p) :
    r ≺i Subrel s (· ∈ p) :=
  ⟨RelEmbedding.codRestrict p f H, ⟨f.top, H₂⟩, fun ⟨_, _⟩ => by simp [← f.mem_range_iff_rel]⟩
        
      

      
        Codomain restriction of a principal segment embedding
        
          Informal description
          Given a principal segment embedding $f : r \prec_i s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, a subset $p$ of $\beta$, and proofs that:
1. For every $a \in \alpha$, $f(a) \in p$ (denoted by $H$), and
2. The top element $f.\text{top}$ of the principal segment is in $p$ (denoted by $H_2$),

the function constructs a principal segment embedding from $r$ to the restriction of $s$ to the subset $p$. 

In other words, it restricts the codomain of the principal segment embedding $f$ to the subset $p$ while preserving the principal segment structure.
        
      
    
  
        
          
    
      PrincipalSeg.codRestrict_apply
      theorem
    
    
      
         (p) (f : r ≺i s) (H H₂ a) : codRestrict p f H H₂ a = ⟨f a, H a⟩
        
          Full source
          @[simp]
theorem codRestrict_apply (p) (f : r ≺i s) (H H₂ a) : codRestrict p f H H₂ a = ⟨f a, H a⟩ :=
  rfl
        
      

      
        Application of Codomain-Restricted Principal Segment Embedding
        
          Informal description
          Let $r$ and $s$ be relations on types $\alpha$ and $\beta$ respectively, and let $f : r \prec_i s$ be a principal segment embedding. Given a subset $p \subseteq \beta$ such that:
1. For every $a \in \alpha$, $f(a) \in p$, and
2. The top element $f.\text{top}$ of the principal segment is in $p$,

then for any $a \in \alpha$, the application of the codomain-restricted principal segment embedding to $a$ equals $\langle f(a), H(a) \rangle$, where $H$ is the proof that $f(a) \in p$.
        
      
    
  
        
          
    
      PrincipalSeg.codRestrict_top
      theorem
    
    
      
         (p) (f : r ≺i s) (H H₂) : (codRestrict p f H H₂).top = ⟨f.top, H₂⟩
        
          Full source
          @[simp]
theorem codRestrict_top (p) (f : r ≺i s) (H H₂) : (codRestrict p f H H₂).top = ⟨f.top, H₂⟩ :=
  rfl
        
      

      
        Top Element Preservation under Codomain Restriction of Principal Segment Embedding
        
          Informal description
          Given a principal segment embedding $f : r \prec_i s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, a subset $p$ of $\beta$, and proofs that:
1. For every $a \in \alpha$, $f(a) \in p$ (denoted by $H$), and
2. The top element $f.\text{top}$ of the principal segment is in $p$ (denoted by $H_2$),

the top element of the codomain-restricted principal segment embedding $\text{codRestrict}\ p\ f\ H\ H_2$ is equal to $\langle f.\text{top}, H_2 \rangle$.
        
      
    
  
        
          
    
      PrincipalSeg.ofIsEmpty
      definition
    
    
      
         (r : α → α → Prop) [IsEmpty α] {b : β} (H : ∀ b', ¬s b' b) : r ≺i s
        
          Full source
          /-- Principal segment from an empty type into a type with a minimal element. -/
def ofIsEmpty (r : α → α → Prop) [IsEmpty α] {b : β} (H : ∀ b', ¬s b' b) : r ≺i s :=
  { RelEmbedding.ofIsEmpty r s with
    top := b
    mem_range_iff_rel' := by simp [H] }
        
      

      
        Principal segment embedding from an empty type
        
          Informal description
          Given a relation $r$ on an empty type $\alpha$ and a relation $s$ on a type $\beta$, for any element $b \in \beta$ such that no element $b' \in \beta$ satisfies $s(b', b)$, there exists a principal segment embedding from $r$ to $s$ with $b$ as the top element of the principal segment.
        
      
    
  
        
          
    
      PrincipalSeg.ofIsEmpty_top
      theorem
    
    
      
         (r : α → α → Prop) [IsEmpty α] {b : β} (H : ∀ b', ¬s b' b) : (ofIsEmpty r H).top = b
        
          Full source
          @[simp]
theorem ofIsEmpty_top (r : α → α → Prop) [IsEmpty α] {b : β} (H : ∀ b', ¬s b' b) :
    (ofIsEmpty r H).top = b :=
  rfl
        
      

      
        Top Element of Principal Segment Embedding from Empty Type
        
          Informal description
          Given a relation $r$ on an empty type $\alpha$ and a relation $s$ on a type $\beta$, for any element $b \in \beta$ such that no element $b' \in \beta$ satisfies $s(b', b)$, the top element of the principal segment embedding constructed via `ofIsEmpty` is equal to $b$.
        
      
    
  
        
          
    
      PrincipalSeg.pemptyToPunit
      abbrev
    
    
      
         : @EmptyRelation PEmpty ≺i @EmptyRelation PUnit
        
          Full source
          /-- Principal segment from the empty relation on `PEmpty` to the empty relation on `PUnit`. -/
abbrev pemptyToPunit : @EmptyRelation PEmpty ≺i @EmptyRelation PUnit :=
  (@ofIsEmpty _ _ EmptyRelation _ _ PUnit.unit) fun _ => not_false
        
      

      
        Principal Segment Embedding from Empty Relation on `PEmpty` to Empty Relation on `PUnit`
        
          Informal description
          There exists a principal segment embedding from the empty relation on the type `PEmpty` to the empty relation on the type `PUnit`.
        
      
    
  
        
          
    
      PrincipalSeg.acc
      theorem
    
    
      
         [IsTrans β s] (f : r ≺i s) (a : α) : Acc r a ↔ Acc s (f a)
        
          Full source
          protected theorem acc [IsTrans β s] (f : r ≺i s) (a : α) : AccAcc r a ↔ Acc s (f a) :=
  (f : r ≼i s).acc a
        
      

      
        Accessibility Preservation under Principal Segment Embeddings
        
          Informal description
          Let $r$ be a relation on $\alpha$ and $s$ a transitive relation on $\beta$. For any principal segment embedding $f \colon r \prec_i s$ and any element $a \in \alpha$, the element $a$ is accessible with respect to $r$ if and only if $f(a)$ is accessible with respect to $s$.

Here, an element $x$ is called *accessible* with respect to a relation $R$ if every descending $R$-chain starting from $x$ is finite.
        
      
    
  
        
          
    
      wellFounded_iff_principalSeg
      theorem
    
    
      
         {β : Type u} {s : β → β → Prop} [IsTrans β s] :
  WellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop) (_ : r ≺i s), WellFounded r
        
          Full source
          theorem wellFounded_iff_principalSeg.{u} {β : Type u} {s : β → β → Prop} [IsTrans β s] :
    WellFoundedWellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop) (_ : r ≺i s), WellFounded r :=
  ⟨fun wf _ _ f => RelHomClass.wellFounded f.toRelEmbedding wf, fun h =>
    wellFounded_iff_wellFounded_subrel.mpr fun b => h _ _ (PrincipalSeg.ofElement s b)⟩
        
      

      
        Well-foundedness Characterization via Principal Segments: $s$ is well-founded $\leftrightarrow$ all $r \prec_i s$ are well-founded
        
          Informal description
          Let $\beta$ be a type with a transitive relation $s$. The relation $s$ is well-founded if and only if for every type $\alpha$ and every relation $r$ on $\alpha$, any principal segment embedding $r \prec_i s$ implies that $r$ is well-founded.
        
      
    
  
        
          
    
      InitialSeg.principalSumRelIso
      definition
    
    
      
         [IsWellOrder β s] (f : r ≼i s) : (r ≺i s) ⊕ (r ≃r s)
        
          Full source
          /-- Every initial segment embedding into a well order can be turned into an isomorphism if
surjective, or into a principal segment embedding if not. -/
noncomputable def principalSumRelIso [IsWellOrder β s] (f : r ≼i s) : (r ≺i s) ⊕ (r ≃r s) :=
  if h : Surjective f
    then Sum.inr (RelIso.ofSurjective f h)
    else Sum.inl (f.toPrincipalSeg h)
        
      

      
        Decomposition of initial segment embedding into principal segment or isomorphism
        
          Informal description
          Given a well-order $s$ on $\beta$ and an initial segment embedding $f : r \preceq_i s$, this function returns either a principal segment embedding $r \prec_i s$ (if $f$ is not surjective) or a relation isomorphism $r \simeq s$ (if $f$ is surjective).
        
      
    
  
        
          
    
      InitialSeg.transPrincipal
      definition
    
    
      
         [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) : r ≺i t
        
          Full source
          /-- Composition of an initial segment embedding and a principal segment embedding as a principal
segment embedding -/
noncomputable def transPrincipal [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) :
    r ≺i t :=
  match f.principalSumRelIso with
  | Sum.inl f' => f'.trans g
  | Sum.inr f' => PrincipalSeg.relIsoTrans f' g
        
      

      
        Composition of initial segment embedding with principal segment embedding
        
          Informal description
          Given a well-order $s$ on $\beta$, a transitive relation $t$ on $\gamma$, an initial segment embedding $f : r \preceq_i s$, and a principal segment embedding $g : s \prec_i t$, the composition of $f$ and $g$ forms a principal segment embedding $r \prec_i t$. 

More precisely, if $f$ decomposes into a principal segment embedding $f' : r \prec_i s$, then the result is the composition $f' \circ g$. If $f$ decomposes into a relation isomorphism $f' : r \simeq s$, then the result is the composition $g \circ f'$.
        
      
    
  
        
          
    
      InitialSeg.transPrincipal_apply
      theorem
    
    
      
         [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) (a : α) : f.transPrincipal g a = g (f a)
        
          Full source
          @[simp]
theorem transPrincipal_apply [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) (a : α) :
    f.transPrincipal g a = g (f a) := by
  rw [InitialSeg.transPrincipal]
  obtain f' | f' := f.principalSumRelIso
  · rw [PrincipalSeg.trans_apply, f.eq_principalSeg]
  · rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]
        
      

      
        Composition Formula for Initial and Principal Segment Embeddings: $(f \circ g)(a) = g(f(a))$
        
          Informal description
          Let $r$, $s$, and $t$ be relations on types $\alpha$, $\beta$, and $\gamma$ respectively, where $s$ is a well-order on $\beta$ and $t$ is a transitive relation on $\gamma$. Given an initial segment embedding $f : r \preceq_i s$ and a principal segment embedding $g : s \prec_i t$, the composition $f \circ g$ evaluated at any element $a \in \alpha$ satisfies $(f \circ g)(a) = g(f(a))$.
        
      
    
  
        
          
    
      RelEmbedding.collapse
      definition
    
    
      
         [IsWellOrder β s] (f : r ↪r s) : r ≼i s
        
          Full source
          /-- 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`. -/
noncomputable def RelEmbedding.collapse [IsWellOrder β s] (f : r ↪r s) : r ≼i s :=
  have H := RelEmbedding.isWellOrder f
  ⟨RelEmbedding.ofMonotone _ fun a b => collapseF_lt f, fun a b h ↦ by
    obtain ⟨m, hm, hm'⟩ := H.wf.has_min { a | ¬s _ b } ⟨_, asymm h⟩
    use m
    obtain lt | rfl | gt := trichotomous_of s b (collapseF f m)
    · refine (collapseF_not_lt f m (fun c h ↦ ?_) lt).elim
      by_contra hn
      exact hm' _ hn h
    · rfl
    · exact (hm gt).elim⟩
        
      

      
        Construction of initial segment embedding via minimal elements
        
          Informal description
          Given a relation embedding $f \colon r \hookrightarrow s$ between relations $r$ on $\alpha$ and $s$ on $\beta$, where $s$ is a well-order on $\beta$, the function constructs an initial segment embedding $r \preceq_i s$ by mapping each element of $\alpha$ to the minimal unused element in $\beta$ that maintains the order structure. This ensures that the range of the resulting embedding forms a lower set in $\beta$ with respect to $s$.
        
      
    
  
        
          
    
      InitialSeg.total
      definition
    
    
      
         (r s) [IsWellOrder α r] [IsWellOrder β s] : (r ≼i s) ⊕ (s ≼i r)
        
          Full source
          /-- For any two well orders, one is an initial segment of the other. -/
noncomputable def InitialSeg.total (r s) [IsWellOrder α r] [IsWellOrder β s] :
    (r ≼i s) ⊕ (s ≼i r) :=
  match (leAdd r s).principalSumRelIso,
    (RelEmbedding.sumLexInr r s).collapse.principalSumRelIso with
  | Sum.inl f, Sum.inr g => Sum.inl <| f.transRelIso g.symm
  | Sum.inr f, Sum.inl g => Sum.inr <| g.transRelIso f.symm
  | Sum.inr f, Sum.inr g => Sum.inl <| (f.trans g.symm).toInitialSeg
  | Sum.inl f, Sum.inl g => Classical.choice <| by
      obtain h | h | h := trichotomous_of (Sum.Lex r s) f.top g.top
      · exact ⟨Sum.inl <| (f.codRestrict {x | Sum.Lex r s x g.top}
          (fun a => _root_.trans (f.lt_top a) h) h).transRelIso g.subrelIso⟩
      · let f := f.subrelIso
        rw [h] at f
        exact ⟨Sum.inl <| (f.symm.trans g.subrelIso).toInitialSeg⟩
      · exact ⟨Sum.inr <| (g.codRestrict {x | Sum.Lex r s x f.top}
          (fun a => _root_.trans (g.lt_top a) h) h).transRelIso f.subrelIso⟩
        
      

      
        Trichotomy theorem for well-orders
        
          Informal description
          For any two well-orders $r$ on $\alpha$ and $s$ on $\beta$, either there exists an initial segment embedding from $r$ to $s$ (denoted $r \preceq_i s$) or there exists an initial segment embedding from $s$ to $r$ (denoted $s \preceq_i r$). This is known as the trichotomy theorem for well-orders.
        
      
    
  
        
          
    
      OrderIso.toInitialSeg
      definition
    
    
      
         [Preorder α] [Preorder β] (f : α ≃o β) : α ≤i β
        
          Full source
          /-- An order isomorphism is an initial segment -/
@[simps!]
def _root_.OrderIso.toInitialSeg [Preorder α] [Preorder β] (f : α ≃o β) : α ≤i β :=
  f.toRelIsoLT.toInitialSeg
        
      

      
        Conversion of Order Isomorphism to Initial Segment Embedding
        
          Informal description
          Given an order isomorphism $f \colon \alpha \simeq_o \beta$ between preordered types $\alpha$ and $\beta$, the function converts $f$ into an initial segment embedding $\alpha \leq_i \beta$ by first converting it to a relation isomorphism on the strict orders and then to an initial segment embedding.
        
      
    
  
        
          
    
      InitialSeg.mem_range_of_le
      theorem
    
    
      
         [LT α] (f : α ≤i β) (h : b ≤ f a) : b ∈ Set.range f
        
          Full source
          theorem mem_range_of_le [LT α] (f : α ≤i β) (h : b ≤ f a) : b ∈ Set.range f := by
  obtain rfl | hb := h.eq_or_lt
  exacts [⟨a, rfl⟩, f.mem_range_of_rel hb]
        
      

      
        Range Membership Property for Initial Segment Embeddings under Inequality
        
          Informal description
          Let $\alpha$ and $\beta$ be types with a less-than relation $<$ on $\alpha$, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. For any elements $a \in \alpha$ and $b \in \beta$, if $b \leq f(a)$, then $b$ belongs to the range of $f$.
        
      
    
  
        
          
    
      InitialSeg.isLowerSet_range
      theorem
    
    
      
         [LT α] (f : α ≤i β) : IsLowerSet (Set.range f)
        
          Full source
          theorem isLowerSet_range [LT α] (f : α ≤i β) : IsLowerSet (Set.range f) := by
  rintro _ b h ⟨a, rfl⟩
  exact mem_range_of_le f h
        
      

      
        Range of Initial Segment Embedding is a Lower Set
        
          Informal description
          Let $\alpha$ and $\beta$ be types equipped with a less-than relation $<$, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. Then the range of $f$ is a lower set, meaning that for any $b \in \beta$ and $a \in \alpha$, if $b < f(a)$, then $b$ belongs to the range of $f$.
        
      
    
  
        
          
    
      InitialSeg.le_iff_le
      theorem
    
    
      
         [PartialOrder α] (f : α ≤i β) : f a ≤ f a' ↔ a ≤ a'
        
          Full source
          @[simp]
theorem le_iff_le [PartialOrder α] (f : α ≤i β) : f a ≤ f a' ↔ a ≤ a' :=
  f.toOrderEmbedding.le_iff_le
        
      

      
        Initial Segment Embedding Preserves Order Relation: $f(a) \leq f(a') \leftrightarrow a \leq a'$
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. Then for any elements $a, a' \in \alpha$, we have $f(a) \leq f(a')$ in $\beta$ if and only if $a \leq a'$ in $\alpha$.
        
      
    
  
        
          
    
      InitialSeg.lt_iff_lt
      theorem
    
    
      
         [PartialOrder α] (f : α ≤i β) : f a < f a' ↔ a < a'
        
          Full source
          @[simp]
theorem lt_iff_lt [PartialOrder α] (f : α ≤i β) : f a < f a' ↔ a < a' :=
  f.toOrderEmbedding.lt_iff_lt
        
      

      
        Initial Segment Embedding Preserves Strict Order
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. Then for any elements $a, a' \in \alpha$, we have $f(a) < f(a')$ in $\beta$ if and only if $a < a'$ in $\alpha$.
        
      
    
  
        
          
    
      InitialSeg.monotone
      theorem
    
    
      
         [PartialOrder α] (f : α ≤i β) : Monotone f
        
          Full source
          theorem monotone [PartialOrder α] (f : α ≤i β) : Monotone f :=
  f.toOrderEmbedding.monotone
        
      

      
        Monotonicity of Initial Segment Embeddings
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. Then $f$ is monotone, meaning that for any $a, a' \in \alpha$, if $a \leq a'$, then $f(a) \leq f(a')$.
        
      
    
  
        
          
    
      InitialSeg.strictMono
      theorem
    
    
      
         [PartialOrder α] (f : α ≤i β) : StrictMono f
        
          Full source
          theorem strictMono [PartialOrder α] (f : α ≤i β) : StrictMono f :=
  f.toOrderEmbedding.strictMono
        
      

      
        Strict Monotonicity of Initial Segment Embeddings
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. Then $f$ is strictly monotone, meaning that for any $x, y \in \alpha$, if $x < y$ then $f(x) < f(y)$ in $\beta$.
        
      
    
  
        
          
    
      InitialSeg.isMin_apply_iff
      theorem
    
    
      
         [PartialOrder α] (f : α ≤i β) : IsMin (f a) ↔ IsMin a
        
          Full source
          @[simp]
theorem isMin_apply_iff [PartialOrder α] (f : α ≤i β) : IsMinIsMin (f a) ↔ IsMin a := by
  refine ⟨StrictMono.isMin_of_apply f.strictMono, fun h b hb ↦ ?_⟩
  obtain ⟨x, rfl⟩ := f.mem_range_of_le hb
  rw [f.le_iff_le] at hb ⊢
  exact h hb
        
      

      
        Minimality Preservation under Initial Segment Embeddings: $f(a)$ is minimal $\leftrightarrow$ $a$ is minimal
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. For any element $a \in \alpha$, the image $f(a)$ is a minimal element in $\beta$ if and only if $a$ is a minimal element in $\alpha$.
        
      
    
  
        
          
    
      InitialSeg.map_bot
      theorem
    
    
      
         [PartialOrder α] [OrderBot α] [OrderBot β] (f : α ≤i β) : f ⊥ = ⊥
        
          Full source
          @[simp]
theorem map_bot [PartialOrder α] [OrderBot α] [OrderBot β] (f : α ≤i β) : f ⊥ = ⊥ :=
  (map_isMin f isMin_bot).eq_bot
        
      

      
        Initial Segment Embedding Preserves Bottom Element: $f(\bot) = \bot$
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. For any initial segment embedding $f \colon \alpha \leq_i \beta$, the image of $\bot_\alpha$ under $f$ is $\bot_\beta$, i.e., $f(\bot_\alpha) = \bot_\beta$.
        
      
    
  
        
          
    
      InitialSeg.image_Iio
      theorem
    
    
      
         [PartialOrder α] (f : α ≤i β) (a : α) : f '' Set.Iio a = Set.Iio (f a)
        
          Full source
          theorem image_Iio [PartialOrder α] (f : α ≤i β) (a : α) : f '' Set.Iio a = Set.Iio (f a) :=
  f.toOrderEmbedding.image_Iio f.isLowerSet_range a
        
      

      
        Image of Left-Infinite Interval under Initial Segment Embedding
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. For any element $a \in \alpha$, the image under $f$ of the open left-infinite interval $(-\infty, a)$ in $\alpha$ is equal to the open left-infinite interval $(-\infty, f(a))$ in $\beta$, i.e.,
$$ f\big((-\infty, a)\big) = (-\infty, f(a)). $$
        
      
    
  
        
          
    
      InitialSeg.le_apply_iff
      theorem
    
    
      
         [PartialOrder α] (f : α ≤i β) : b ≤ f a ↔ ∃ c ≤ a, f c = b
        
          Full source
          theorem le_apply_iff [PartialOrder α] (f : α ≤i β) : b ≤ f a ↔ ∃ c ≤ a, f c = b := by
  constructor
  · intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_le h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.le_iff_le] at h
  · rintro ⟨c, hc, rfl⟩
    exact f.monotone hc
        
      

      
        Characterization of Order Relation via Initial Segment Embedding: $b \leq f(a) \leftrightarrow \exists c \leq a, f(c) = b$
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. For any elements $a \in \alpha$ and $b \in \beta$, we have $b \leq f(a)$ if and only if there exists $c \in \alpha$ with $c \leq a$ such that $f(c) = b$.
        
      
    
  
        
          
    
      InitialSeg.lt_apply_iff
      theorem
    
    
      
         [PartialOrder α] (f : α ≤i β) : b < f a ↔ ∃ a' < a, f a' = b
        
          Full source
          theorem lt_apply_iff [PartialOrder α] (f : α ≤i β) : b < f a ↔ ∃ a' < a, f a' = b := by
  constructor
  · intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_rel h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.lt_iff_lt] at h
  · rintro ⟨c, hc, rfl⟩
    exact f.strictMono hc
        
      

      
        Characterization of Elements Below Initial Segment Embedding
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \leq_i \beta$ be an initial segment embedding. For any $a \in \alpha$ and $b \in \beta$, we have $b < f(a)$ if and only if there exists $a' \in \alpha$ with $a' < a$ such that $f(a') = b$.
        
      
    
  
        
          
    
      PrincipalSeg.mem_range_of_le
      theorem
    
    
      
         [LT α] (f : α <i β) (h : b ≤ f a) : b ∈ Set.range f
        
          Full source
          theorem mem_range_of_le [LT α] (f : α <i β) (h : b ≤ f a) : b ∈ Set.range f :=
  (f : α ≤i β).mem_range_of_le h
        
      

      
        Elements Below Images in Principal Segment Embedding Belong to Range
        
          Informal description
          Let $\alpha$ and $\beta$ be types equipped with a less-than relation $<$, and let $f \colon \alpha <_i \beta$ be a principal segment embedding. For any elements $a \in \alpha$ and $b \in \beta$, if $b \leq f(a)$, then $b$ belongs to the range of $f$.
        
      
    
  
        
          
    
      PrincipalSeg.isLowerSet_range
      theorem
    
    
      
         [LT α] (f : α <i β) : IsLowerSet (Set.range f)
        
          Full source
          theorem isLowerSet_range [LT α] (f : α <i β) : IsLowerSet (Set.range f) :=
  (f : α ≤i β).isLowerSet_range
        
      

      
        Range of Principal Segment Embedding is a Lower Set
        
          Informal description
          Let $\alpha$ and $\beta$ be types equipped with a less-than relation $<$, and let $f \colon \alpha <_i \beta$ be a principal segment embedding. Then the range of $f$ is a lower set, meaning that for any $b \in \beta$ and $a \in \alpha$, if $b < f(a)$, then $b$ belongs to the range of $f$.
        
      
    
  
        
          
    
      PrincipalSeg.le_iff_le
      theorem
    
    
      
         [PartialOrder α] (f : α <i β) : f a ≤ f a' ↔ a ≤ a'
        
          Full source
          @[simp]
theorem le_iff_le [PartialOrder α] (f : α <i β) : f a ≤ f a' ↔ a ≤ a' :=
  (f : α ≤i β).le_iff_le
        
      

      
        Principal Segment Embedding Preserves Order Relation: $f(a) \leq f(a') \leftrightarrow a \leq a'$
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \prec_i \beta$ be a principal segment embedding. Then for any elements $a, a' \in \alpha$, we have $f(a) \leq f(a')$ in $\beta$ if and only if $a \leq a'$ in $\alpha$.
        
      
    
  
        
          
    
      PrincipalSeg.lt_iff_lt
      theorem
    
    
      
         [PartialOrder α] (f : α <i β) : f a < f a' ↔ a < a'
        
          Full source
          @[simp]
theorem lt_iff_lt [PartialOrder α] (f : α <i β) : f a < f a' ↔ a < a' :=
  (f : α ≤i β).lt_iff_lt
        
      

      
        Principal Segment Embedding Preserves Strict Order
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha <_i \beta$ be a principal segment embedding. Then for any elements $a, a' \in \alpha$, we have $f(a) < f(a')$ in $\beta$ if and only if $a < a'$ in $\alpha$.
        
      
    
  
        
          
    
      PrincipalSeg.monotone
      theorem
    
    
      
         [PartialOrder α] (f : α <i β) : Monotone f
        
          Full source
          theorem monotone [PartialOrder α] (f : α <i β) : Monotone f :=
  (f : α ≤i β).monotone
        
      

      
        Monotonicity of Principal Segment Embeddings
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha <_i \beta$ be a principal segment embedding. Then $f$ is monotone, meaning that for any $a, a' \in \alpha$, if $a \leq a'$, then $f(a) \leq f(a')$.
        
      
    
  
        
          
    
      PrincipalSeg.strictMono
      theorem
    
    
      
         [PartialOrder α] (f : α <i β) : StrictMono f
        
          Full source
          theorem strictMono [PartialOrder α] (f : α <i β) : StrictMono f :=
  (f : α ≤i β).strictMono
        
      

      
        Strict Monotonicity of Principal Segment Embeddings
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \prec_i \beta$ be a principal segment embedding. Then $f$ is strictly monotone, meaning that for any $x, y \in \alpha$, if $x < y$ then $f(x) < f(y)$ in $\beta$.
        
      
    
  
        
          
    
      PrincipalSeg.isMin_apply_iff
      theorem
    
    
      
         [PartialOrder α] (f : α <i β) : IsMin (f a) ↔ IsMin a
        
          Full source
          @[simp]
theorem isMin_apply_iff [PartialOrder α] (f : α <i β) : IsMinIsMin (f a) ↔ IsMin a :=
  (f : α ≤i β).isMin_apply_iff
        
      

      
        Minimality Preservation under Principal Segment Embeddings: $f(a)$ is minimal $\leftrightarrow$ $a$ is minimal
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha \prec_i \beta$ be a principal segment embedding. For any element $a \in \alpha$, the image $f(a)$ is a minimal element in $\beta$ if and only if $a$ is a minimal element in $\alpha$.
        
      
    
  
        
          
    
      PrincipalSeg.map_bot
      theorem
    
    
      
         [PartialOrder α] [OrderBot α] [OrderBot β] (f : α <i β) : f ⊥ = ⊥
        
          Full source
          @[simp]
theorem map_bot [PartialOrder α] [OrderBot α] [OrderBot β] (f : α <i β) : f ⊥ = ⊥ :=
  (f : α ≤i β).map_bot
        
      

      
        Principal Segment Embedding Preserves Bottom Element: $f(\bot) = \bot$
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets with bottom elements $\bot_\alpha$ and $\bot_\beta$ respectively. For any principal segment embedding $f \colon \alpha \prec_i \beta$, the image of $\bot_\alpha$ under $f$ is $\bot_\beta$, i.e., $f(\bot_\alpha) = \bot_\beta$.
        
      
    
  
        
          
    
      PrincipalSeg.image_Iio
      theorem
    
    
      
         [PartialOrder α] (f : α <i β) (a : α) : f '' Set.Iio a = Set.Iio (f a)
        
          Full source
          theorem image_Iio [PartialOrder α] (f : α <i β) (a : α) : f '' Set.Iio a = Set.Iio (f a) :=
  (f : α ≤i β).image_Iio a
        
      

      
        Image of Left-Infinite Interval under Principal Segment Embedding
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha <_i \beta$ be a principal segment embedding. For any element $a \in \alpha$, the image under $f$ of the open left-infinite interval $(-\infty, a)$ in $\alpha$ is equal to the open left-infinite interval $(-\infty, f(a))$ in $\beta$, i.e.,
$$ f\big((-\infty, a)\big) = (-\infty, f(a)). $$
        
      
    
  
        
          
    
      PrincipalSeg.le_apply_iff
      theorem
    
    
      
         [PartialOrder α] (f : α <i β) : b ≤ f a ↔ ∃ c ≤ a, f c = b
        
          Full source
          theorem le_apply_iff [PartialOrder α] (f : α <i β) : b ≤ f a ↔ ∃ c ≤ a, f c = b :=
  (f : α ≤i β).le_apply_iff
        
      

      
        Characterization of Order Relation via Principal Segment Embedding: $b \leq f(a) \leftrightarrow \exists c \leq a, f(c) = b$
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha <_i \beta$ be a principal segment embedding. For any elements $a \in \alpha$ and $b \in \beta$, we have $b \leq f(a)$ if and only if there exists $c \in \alpha$ with $c \leq a$ such that $f(c) = b$.
        
      
    
  
        
          
    
      PrincipalSeg.lt_apply_iff
      theorem
    
    
      
         [PartialOrder α] (f : α <i β) : b < f a ↔ ∃ a' < a, f a' = b
        
          Full source
          theorem lt_apply_iff [PartialOrder α] (f : α <i β) : b < f a ↔ ∃ a' < a, f a' = b :=
  (f : α ≤i β).lt_apply_iff
        
      

      
        Characterization of Elements Below Principal Segment Embedding
        
          Informal description
          Let $\alpha$ and $\beta$ be partially ordered sets, and let $f \colon \alpha <_i \beta$ be a principal segment embedding. For any $a \in \alpha$ and $b \in \beta$, we have $b < f(a)$ if and only if there exists $a' \in \alpha$ with $a' < a$ such that $f(a') = b$.