Documentation

Mathlib.Order.InitialSeg

Initial and principal segments #

This file defines initial and principal segments.

Main definitions #

Notations #

These notations belong to the InitialSeg locale.

Initial segments #

Order embeddings whose range is an initial segment of s (i.e., if b belongs to the range, then any b' < b also belongs to the range). The type of these embeddings from r to s is called InitialSeg r s, and denoted by r ≼i s≼i s.

structure InitialSeg {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) extends RelEmbedding :
Type (maxu_1u_2)
  • The order embedding is an initial segment

    init' : ∀ (a : α) (b : β), s b (toRelEmbedding.toEmbedding a)a', toRelEmbedding.toEmbedding a' = b

If r is a relation on α and s in a relation on β, then f : r ≼i s≼i s is an order embedding whose range is an initial segment. That is, whenever b < f a in β then b is in the range of f.

Instances For

    If r is a relation on α and s in a relation on β, then f : r ≼i s≼i s is an order embedding whose range is an initial segment. That is, whenever b < f a in β then b is in the range of f.

    Equations
    instance InitialSeg.instCoeInitialSegRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
    Coe (r ≼i s) (r ↪r s)
    Equations
    • InitialSeg.instCoeInitialSegRelEmbedding = { coe := InitialSeg.toRelEmbedding }
    instance InitialSeg.instEmbeddingLikeInitialSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
    EmbeddingLike (r ≼i s) α β
    Equations
    theorem InitialSeg.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ≼i s} {g : r ≼i s} (h : ∀ (x : α), f x = g x) :
    f = g
    @[simp]
    theorem InitialSeg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≼i s) :
    f.toRelEmbedding.toEmbedding = f
    theorem InitialSeg.init {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≼i s) {a : α} {b : β} :
    s b (f a)a', f a' = b
    theorem InitialSeg.map_rel_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {a : α} {b : α} (f : r ≼i s) :
    s (f a) (f b) r a b
    theorem InitialSeg.init_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≼i s) {a : α} {b : β} :
    s b (f a) a', f a' = b r a' a
    def InitialSeg.ofIso {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :
    r ≼i s

    An order isomorphism is an initial segment

    Equations
    • One or more equations did not get rendered due to their size.
    def InitialSeg.refl {α : Type u_1} (r : ααProp) :
    r ≼i r

    The identity function shows that ≼i≼i is reflexive

    Equations
    • One or more equations did not get rendered due to their size.
    instance InitialSeg.instInhabitedInitialSeg {α : Type u_1} (r : ααProp) :
    Equations
    def InitialSeg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≼i s) (g : s ≼i t) :
    r ≼i t

    Composition of functions shows that ≼i≼i is transitive

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem InitialSeg.refl_apply {α : Type u_1} {r : ααProp} (x : α) :
    ↑(InitialSeg.refl r) x = x
    @[simp]
    theorem InitialSeg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≼i s) (g : s ≼i t) (a : α) :
    ↑(InitialSeg.trans f g) a = g (f a)
    theorem InitialSeg.unique_of_trichotomous_of_irrefl {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsTrichotomous β s] [inst : IsIrrefl β s] :
    theorem InitialSeg.eq {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ≼i s) (g : r ≼i s) (a : α) :
    f a = g a
    theorem InitialSeg.Antisymm.aux {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsWellOrder α r] (f : r ≼i s) (g : s ≼i r) :
    def InitialSeg.antisymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ≼i s) (g : s ≼i 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
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem InitialSeg.antisymm_toFun {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) :
    (RelIso.toRelEmbedding (InitialSeg.antisymm f g)).toEmbedding = f
    @[simp]
    theorem InitialSeg.antisymm_symm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsWellOrder α r] [inst : IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) :
    theorem InitialSeg.eq_or_principal {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ≼i s) :
    Function.Surjective f b, ∀ (x : β), s x b y, f y = x
    def InitialSeg.codRestrict {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : r ≼i s) (H : ∀ (a : α), f a p) :
    r ≼i Subrel s p

    Restrict the codomain of an initial segment

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem InitialSeg.codRestrict_apply {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} (p : Set β) (f : r ≼i s) (H : ∀ (a : α), f a p) (a : α) :
    ↑(InitialSeg.codRestrict p f H) a = { val := f a, property := H a }
    def InitialSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [inst : IsEmpty α] :
    r ≼i s

    Initial segment from an empty type.

    Equations
    • One or more equations did not get rendered due to their size.
    def InitialSeg.leAdd {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem InitialSeg.leAdd_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (a : α) :

    Principal segments #

    Order embeddings whose range is a principal segment of s (i.e., an interval of the form (-∞, top)∞, top) for some element top of β). The type of these embeddings from r to s is called PrincipalSeg r s, and denoted by r ≺i s≺i s. Principal segments are in particular initial segments.

    structure PrincipalSeg {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) extends RelEmbedding :
    Type (maxu_1u_2)
    • The supremum of the principal segment

      top : β
    • The image of the order embedding is the set of elements b such that s b top

      down' : ∀ (b : β), s b top a, toRelEmbedding.toEmbedding a = b

    If r is a relation on α and s in a relation on β, then f : r ≺i s≺i s is an order embedding whose range is an open interval (-∞, top)∞, top) for some element top of β. Such order embeddings are called principal segments

    Instances For

      If r is a relation on α and s in a relation on β, then f : r ≺i s≺i s is an order embedding whose range is an open interval (-∞, top)∞, top) for some element top of β. Such order embeddings are called principal segments

      Equations
      instance PrincipalSeg.instCoeOutPrincipalSegRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
      CoeOut (r ≺i s) (r ↪r s)
      Equations
      • PrincipalSeg.instCoeOutPrincipalSegRelEmbedding = { coe := PrincipalSeg.toRelEmbedding }
      instance PrincipalSeg.instCoeFunPrincipalSegForAll {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
      CoeFun (r ≺i s) fun x => αβ
      Equations
      • PrincipalSeg.instCoeFunPrincipalSegForAll = { coe := fun f => f.toRelEmbedding.toEmbedding }
      @[simp]
      theorem PrincipalSeg.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.toEmbedding a = b) :
      { toRelEmbedding := f, top := t, down' := o }.toRelEmbedding.toEmbedding = f.toEmbedding
      theorem PrincipalSeg.down {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≺i s) {b : β} :
      s b f.top a, f.toRelEmbedding.toEmbedding a = b
      theorem PrincipalSeg.lt_top {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≺i s) (a : α) :
      s (f.toRelEmbedding.toEmbedding a) f.top
      theorem PrincipalSeg.init {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsTrans β s] (f : r ≺i s) {a : α} {b : β} (h : s b (f.toRelEmbedding.toEmbedding a)) :
      a', f.toRelEmbedding.toEmbedding a' = b
      instance PrincipalSeg.hasCoeInitialSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsTrans β s] :
      Coe (r ≺i s) (r ≼i s)

      A principal segment is in particular an initial segment.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem PrincipalSeg.coe_coe_fn' {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsTrans β s] (f : r ≺i s) :
      { toRelEmbedding := f.toRelEmbedding, init' := (_ : ∀ (x : α) (x_1 : β), s x_1 (f.toRelEmbedding.toEmbedding x)a', f.toRelEmbedding.toEmbedding a' = x_1) } = f.toRelEmbedding.toEmbedding
      theorem PrincipalSeg.init_iff {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsTrans β s] (f : r ≺i s) {a : α} {b : β} :
      s b (f.toRelEmbedding.toEmbedding a) a', f.toRelEmbedding.toEmbedding a' = b r a' a
      theorem PrincipalSeg.irrefl {α : Type u_1} {r : ααProp} [inst : IsWellOrder α r] (f : r ≺i r) :
      def PrincipalSeg.ltLe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≺i s) (g : s ≼i t) :
      r ≺i t

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem PrincipalSeg.lt_le_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≺i s) (g : s ≼i t) (a : α) :
      (PrincipalSeg.ltLe f g).toRelEmbedding.toEmbedding a = g (f.toRelEmbedding.toEmbedding a)
      @[simp]
      theorem PrincipalSeg.lt_le_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≺i s) (g : s ≼i t) :
      (PrincipalSeg.ltLe f g).top = g f.top
      def PrincipalSeg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [inst : IsTrans γ t] (f : r ≺i s) (g : s ≺i t) :
      r ≺i t

      Composition of two principal segments as a principal segment

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem PrincipalSeg.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_1} {r : ααProp} {s : ββProp} {t : γγProp} [inst : IsTrans γ t] (f : r ≺i s) (g : s ≺i t) (a : α) :
      (PrincipalSeg.trans f g).toRelEmbedding.toEmbedding a = g.toRelEmbedding.toEmbedding (f.toRelEmbedding.toEmbedding a)
      @[simp]
      theorem PrincipalSeg.trans_top {α : Type u_2} {β : Type u_3} {γ : Type u_1} {r : ααProp} {s : ββProp} {t : γγProp} [inst : IsTrans γ t] (f : r ≺i s) (g : s ≺i t) :
      (PrincipalSeg.trans f g).top = g.toRelEmbedding.toEmbedding f.top
      def PrincipalSeg.equivLT {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≃r s) (g : s ≺i t) :
      r ≺i t

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

      Equations
      • One or more equations did not get rendered due to their size.
      def PrincipalSeg.ltEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≺i s) (g : s ≃r t) :
      r ≺i t

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem PrincipalSeg.equivLT_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≃r s) (g : s ≺i t) (a : α) :
      (PrincipalSeg.equivLT f g).toRelEmbedding.toEmbedding a = g.toRelEmbedding.toEmbedding ((RelIso.toRelEmbedding f).toEmbedding a)
      @[simp]
      theorem PrincipalSeg.equivLT_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≃r s) (g : s ≺i t) :
      (PrincipalSeg.equivLT f g).top = g.top
      instance PrincipalSeg.instSubsingletonPrincipalSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] :

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

      Equations
      theorem PrincipalSeg.top_eq {α : Type u_2} {β : Type u_3} {γ : Type u_1} {r : ααProp} {s : ββProp} {t : γγProp} [inst : IsWellOrder γ t] (e : r ≃r s) (f : r ≺i t) (g : s ≺i t) :
      f.top = g.top
      theorem PrincipalSeg.topLTTop {α : Type u_2} {β : Type u_3} {γ : Type u_1} {r : ααProp} {s : ββProp} {t : γγProp} [inst : IsWellOrder γ t] (f : r ≺i s) (g : s ≺i t) (h : r ≺i t) :
      t h.top g.top
      def PrincipalSeg.ofElement {α : Type u_1} (r : ααProp) (a : α) :
      Subrel r { b | r b a } ≺i r

      Any element of a well order yields a principal segment

      Equations
      @[simp]
      theorem PrincipalSeg.ofElement_apply {α : Type u_1} (r : ααProp) (a : α) (b : { b | r b a }) :
      (PrincipalSeg.ofElement r a).toRelEmbedding.toEmbedding b = b
      @[simp]
      theorem PrincipalSeg.ofElement_top {α : Type u_1} (r : ααProp) (a : α) :
      def PrincipalSeg.codRestrict {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : r ≺i s) (H : ∀ (a : α), f.toRelEmbedding.toEmbedding a p) (H₂ : f.top p) :
      r ≺i Subrel s p

      Restrict the codomain of a principal segment

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem PrincipalSeg.codRestrict_apply {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} (p : Set β) (f : r ≺i s) (H : ∀ (a : α), f.toRelEmbedding.toEmbedding a p) (H₂ : f.top p) (a : α) :
      (PrincipalSeg.codRestrict p f H H₂).toRelEmbedding.toEmbedding a = { val := f.toRelEmbedding.toEmbedding a, property := H a }
      @[simp]
      theorem PrincipalSeg.codRestrict_top {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} (p : Set β) (f : r ≺i s) (H : ∀ (a : α), f.toRelEmbedding.toEmbedding a p) (H₂ : f.top p) :
      (PrincipalSeg.codRestrict p f H H₂).top = { val := f.top, property := H₂ }
      def PrincipalSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) [inst : IsEmpty α] {b : β} (H : ∀ (b' : β), ¬s b' b) :
      r ≺i s

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem PrincipalSeg.ofIsEmpty_top {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) [inst : IsEmpty α] {b : β} (H : ∀ (b' : β), ¬s b' b) :
      def PrincipalSeg.pemptyToPunit :
      EmptyRelation ≺i EmptyRelation

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

      Equations

      Properties of initial and principal segments #

      noncomputable def InitialSeg.ltOrEq {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ≼i s) :
      (r ≺i 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
      • One or more equations did not get rendered due to their size.
      theorem InitialSeg.ltOrEq_apply_left {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ≼i s) (g : r ≺i s) (a : α) :
      g.toRelEmbedding.toEmbedding a = f a
      theorem InitialSeg.ltOrEq_apply_right {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ≼i s) (g : r ≃r s) (a : α) :
      (RelIso.toRelEmbedding g).toEmbedding a = f a
      noncomputable def InitialSeg.leLT {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [inst : IsWellOrder β s] [inst : IsTrans γ t] (f : r ≼i s) (g : s ≺i t) :
      r ≺i t

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

      Equations
      @[simp]
      theorem InitialSeg.leLT_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} {r : ααProp} {s : ββProp} {t : γγProp} [inst : IsWellOrder β s] [inst : IsTrans γ t] (f : r ≼i s) (g : s ≺i t) (a : α) :
      (InitialSeg.leLT f g).toRelEmbedding.toEmbedding a = g.toRelEmbedding.toEmbedding (f a)
      noncomputable def RelEmbedding.collapseF {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ↪r s) (a : α) :
      { b // ¬s (f.toEmbedding 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
      • One or more equations did not get rendered due to their size.
      theorem RelEmbedding.collapseF.lt {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ↪r s) {a : α} {a' : α} :
      r a' as ↑(RelEmbedding.collapseF f a') ↑(RelEmbedding.collapseF f a)
      theorem RelEmbedding.collapseF.not_lt {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ↪r s) (a : α) {b : β} (h : (a' : α) → r a' as (↑(RelEmbedding.collapseF f a')) b) :
      noncomputable def RelEmbedding.collapse {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ↪r s) :
      r ≼i s

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

      Equations
      • One or more equations did not get rendered due to their size.
      theorem RelEmbedding.collapse_apply {α : Type u_2} {β : Type u_1} {r : ααProp} {s : ββProp} [inst : IsWellOrder β s] (f : r ↪r s) (a : α) :