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.

structure InitialSeg {α : Type u_4} {β : Type u_5} (r : ααProp) (s : ββProp) extends RelEmbedding :
Type (max u_4 u_5)

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

  • toFun : αβ
  • inj' : Function.Injective self.toFun
  • map_rel_iff' : ∀ {a b : α}, s (self.toEmbedding a) (self.toEmbedding b) r a b
  • mem_range_of_rel' : ∀ (a : α) (b : β), s b (self.toRelEmbedding a)b Set.range self.toRelEmbedding

    The order embedding is an initial segment

Instances For
    theorem InitialSeg.mem_range_of_rel' {α : Type u_4} {β : Type u_5} {r : ααProp} {s : ββProp} (self : r ≼i s) (a : α) (b : β) :
    s b (self.toRelEmbedding a)b Set.range self.toRelEmbedding

    The order embedding is an initial segment

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

    Equations
    Instances For
      instance InitialSeg.instCoeRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
      Coe (r ≼i s) (r ↪r s)
      Equations
      • InitialSeg.instCoeRelEmbedding = { coe := InitialSeg.toRelEmbedding }
      instance InitialSeg.instFunLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
      FunLike (r ≼i s) α β
      Equations
      • InitialSeg.instFunLike = { coe := fun (f : r ≼i s) => f.toFun, coe_injective' := }
      instance InitialSeg.instEmbeddingLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
      EmbeddingLike (r ≼i s) α β
      Equations
      • =
      theorem InitialSeg.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f : r ≼i s} {g : r ≼i s} :
      f = g ∀ (x : α), f x = g x
      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 = f
      theorem InitialSeg.mem_range_of_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≼i s) {a : α} {b : β} :
      s b (f a)b Set.range f
      @[deprecated InitialSeg.mem_range_of_rel]
      theorem InitialSeg.init {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≼i s) {a : α} {b : β} :
      s b (f a)b Set.range f

      Alias of InitialSeg.mem_range_of_rel.

      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.exists_eq_iff_rel {α : 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
      @[deprecated InitialSeg.exists_eq_iff_rel]
      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

      Alias of InitialSeg.exists_eq_iff_rel.

      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
      • InitialSeg.ofIso f = { toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := }
      Instances For
        def InitialSeg.refl {α : Type u_1} (r : ααProp) :
        r ≼i r

        The identity function shows that ≼i is reflexive

        Equations
        Instances For
          instance InitialSeg.instInhabited {α : 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 is transitive

          Equations
          • f.trans g = { toRelEmbedding := f.trans g.toRelEmbedding, mem_range_of_rel' := }
          Instances For
            @[simp]
            theorem InitialSeg.refl_apply {α : Type u_1} {r : ααProp} (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 : α) :
            (f.trans g) a = g (f a)
            instance InitialSeg.subsingleton_of_trichotomous_of_irrefl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrichotomous β s] [IsIrrefl β s] [IsWellFounded α r] :
            Equations
            • =
            instance InitialSeg.instSubsingletonOfIsWellOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] :
            Equations
            • =
            theorem InitialSeg.eq {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [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} [IsWellOrder α r] (f : r ≼i s) (g : s ≼i r) :
            def InitialSeg.antisymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [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
            • f.antisymm g = { toFun := f, invFun := g, left_inv := , right_inv := , map_rel_iff' := }
            Instances For
              @[simp]
              theorem InitialSeg.antisymm_toFun {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) :
              (f.antisymm g) = f
              @[simp]
              theorem InitialSeg.antisymm_symm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (f : r ≼i s) (g : s ≼i r) :
              (f.antisymm g).symm = g.antisymm f
              theorem InitialSeg.eq_or_principal {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [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
              Instances For
                @[simp]
                theorem InitialSeg.codRestrict_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : r ≼i s) (H : ∀ (a : α), f a p) (a : α) :
                (InitialSeg.codRestrict p f H) a = f a,
                def InitialSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsEmpty α] :
                r ≼i s

                Initial segment from an empty type.

                Equations
                Instances For
                  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
                  • InitialSeg.leAdd r s = { toFun := Sum.inl, inj' := , map_rel_iff' := , mem_range_of_rel' := }
                  Instances For
                    @[simp]
                    theorem InitialSeg.leAdd_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (a : α) :
                    theorem InitialSeg.acc {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≼i s) (a : α) :
                    Acc r a Acc s (f a)

                    Principal segments #

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

                    structure PrincipalSeg {α : Type u_4} {β : Type u_5} (r : ααProp) (s : ββProp) extends RelEmbedding :
                    Type (max u_4 u_5)

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

                    • toFun : αβ
                    • inj' : Function.Injective self.toFun
                    • map_rel_iff' : ∀ {a b : α}, s (self.toEmbedding a) (self.toEmbedding b) r a b
                    • top : β

                      The supremum of the principal segment

                    • down' : ∀ (b : β), s b self.top ∃ (a : α), self.toRelEmbedding a = b

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

                    Instances For
                      theorem PrincipalSeg.down' {α : Type u_4} {β : Type u_5} {r : ααProp} {s : ββProp} (self : r ≺i s) (b : β) :
                      s b self.top ∃ (a : α), self.toRelEmbedding a = b

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

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

                      Equations
                      Instances For
                        instance PrincipalSeg.instCoeOutRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                        CoeOut (r ≺i s) (r ↪r s)
                        Equations
                        • PrincipalSeg.instCoeOutRelEmbedding = { coe := PrincipalSeg.toRelEmbedding }
                        instance PrincipalSeg.instCoeFunForall {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                        CoeFun (r ≺i s) fun (x : r ≺i s) => αβ
                        Equations
                        • PrincipalSeg.instCoeFunForall = { coe := fun (f : r ≺i s) => f.toRelEmbedding }
                        @[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 a = b) :
                        { toRelEmbedding := f, top := t, down' := o }.toRelEmbedding = f
                        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 a = b
                        theorem PrincipalSeg.lt_top {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≺i s) (a : α) :
                        s (f.toRelEmbedding a) f.top
                        theorem PrincipalSeg.mem_range_of_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : r ≺i s) {a : α} {b : β} (h : s b (f.toRelEmbedding a)) :
                        b Set.range f.toRelEmbedding
                        @[deprecated PrincipalSeg.mem_range_of_rel]
                        theorem PrincipalSeg.init {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : r ≺i s) {a : α} {b : β} (h : s b (f.toRelEmbedding a)) :
                        b Set.range f.toRelEmbedding

                        Alias of PrincipalSeg.mem_range_of_rel.

                        instance PrincipalSeg.hasCoeInitialSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] :
                        Coe (r ≺i s) (r ≼i s)

                        A principal segment is in particular an initial segment.

                        Equations
                        • PrincipalSeg.hasCoeInitialSeg = { coe := fun (f : r ≺i s) => { toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := } }
                        theorem PrincipalSeg.coe_coe_fn' {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : r ≺i s) :
                        { toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := } = f.toRelEmbedding
                        theorem PrincipalSeg.exists_eq_iff_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : r ≺i s) {a : α} {b : β} :
                        s b (f.toRelEmbedding a) ∃ (a' : α), f.toRelEmbedding a' = b r a' a
                        @[deprecated PrincipalSeg.exists_eq_iff_rel]
                        theorem PrincipalSeg.init_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : r ≺i s) {a : α} {b : β} :
                        s b (f.toRelEmbedding a) ∃ (a' : α), f.toRelEmbedding a' = b r a' a

                        Alias of PrincipalSeg.exists_eq_iff_rel.

                        noncomputable def InitialSeg.toPrincipalSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ≼i s) (hf : ¬Function.Surjective f) :
                        r ≺i s

                        A principal segment is the same as a non-surjective initial segment.

                        Equations
                        • f.toPrincipalSeg hf = { toRelEmbedding := f.toRelEmbedding, top := Classical.choose , down' := }
                        Instances For
                          @[simp]
                          theorem InitialSeg.toPrincipalSeg_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ≼i s) (hf : ¬Function.Surjective f) (x : α) :
                          (f.toPrincipalSeg hf).toRelEmbedding x = f x
                          theorem PrincipalSeg.irrefl {α : Type u_1} {r : ααProp} [IsWellOrder α r] (f : r ≺i r) :
                          instance PrincipalSeg.instIsEmptyOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                          Equations
                          • =
                          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
                          • f.ltLe g = { toRelEmbedding := f.trans g.toRelEmbedding, top := g f.top, down' := }
                          Instances For
                            @[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 : α) :
                            (f.ltLe g).toRelEmbedding a = g (f.toRelEmbedding 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) :
                            (f.ltLe g).top = g f.top
                            def PrincipalSeg.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) :
                            r ≺i t

                            Composition of two principal segments as a principal segment

                            Equations
                            • f.trans g = f.ltLe { toRelEmbedding := g.toRelEmbedding, mem_range_of_rel' := }
                            Instances For
                              @[simp]
                              theorem PrincipalSeg.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) (a : α) :
                              (f.trans g).toRelEmbedding a = g.toRelEmbedding (f.toRelEmbedding a)
                              @[simp]
                              theorem PrincipalSeg.trans_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsTrans γ t] (f : r ≺i s) (g : s ≺i t) :
                              (f.trans g).top = g.toRelEmbedding 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
                              • PrincipalSeg.equivLT f g = { toRelEmbedding := f.toRelEmbedding.trans g.toRelEmbedding, top := g.top, down' := }
                              Instances For
                                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
                                • f.ltEquiv g = { toRelEmbedding := f.trans g.toRelEmbedding, top := g f.top, down' := }
                                Instances For
                                  @[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 a = g.toRelEmbedding (f 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.instSubsingletonOfIsWellOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [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_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsWellOrder γ t] (e : r ≃r s) (f : r ≺i t) (g : s ≺i t) :
                                  f.top = g.top
                                  theorem PrincipalSeg.topLTTop {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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
                                  def PrincipalSeg.ofElement {α : Type u_4} (r : ααProp) (a : α) :
                                  Subrel r {b : α | r b a} ≺i r

                                  Any element of a well order yields a principal segment

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem PrincipalSeg.ofElement_apply {α : Type u_4} (r : ααProp) (a : α) (b : {b : α | r b a}) :
                                    (PrincipalSeg.ofElement r a).toRelEmbedding b = b
                                    @[simp]
                                    theorem PrincipalSeg.ofElement_top {α : Type u_4} (r : ααProp) (a : α) :
                                    @[simp]
                                    theorem PrincipalSeg.subrelIso_symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≺i s) :
                                    ∀ (a : α), f.subrelIso.symm a = (Equiv.setCongr ) f.toRelEmbedding a,
                                    noncomputable def PrincipalSeg.subrelIso {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≺i s) :
                                    Subrel s {b : β | s b f.top} ≃r r

                                    For any principal segment r ≺i s, there is a Subrel of s order isomorphic to r.

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

                                      Restrict the codomain of a principal segment

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem PrincipalSeg.codRestrict_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : r ≺i s) (H : ∀ (a : α), f.toRelEmbedding a p) (H₂ : f.top p) (a : α) :
                                        (PrincipalSeg.codRestrict p f H H₂).toRelEmbedding a = f.toRelEmbedding a,
                                        @[simp]
                                        theorem PrincipalSeg.codRestrict_top {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : r ≺i s) (H : ∀ (a : α), f.toRelEmbedding a p) (H₂ : f.top p) :
                                        (PrincipalSeg.codRestrict p f H H₂).top = f.top, H₂
                                        def PrincipalSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) [IsEmpty α] {b : β} (H : ∀ (b' : β), ¬s b' b) :
                                        r ≺i s

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

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem PrincipalSeg.ofIsEmpty_top {α : Type u_1} {β : Type u_2} {s : ββProp} (r : ααProp) [IsEmpty α] {b : β} (H : ∀ (b' : β), ¬s b' b) :
                                          @[reducible, inline]
                                          abbrev PrincipalSeg.pemptyToPunit :
                                          EmptyRelation ≺i EmptyRelation

                                          Principal segment from the empty relation on PEmpty to the empty relation on PUnit.

                                          Equations
                                          Instances For
                                            theorem PrincipalSeg.acc {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : r ≺i s) (a : α) :
                                            Acc r a Acc s (f.toRelEmbedding a)
                                            theorem wellFounded_iff_wellFounded_subrel {β : Type u_4} {s : ββProp} [IsTrans β s] :
                                            WellFounded s ∀ (b : β), WellFounded (Subrel s {b' : β | s b' b})

                                            A relation is well-founded iff every principal segment of it is well-founded.

                                            In this lemma we use Subrel to indicate its principal segments because it's usually more convenient to use.

                                            theorem wellFounded_iff_principalSeg {β : Type u} {s : ββProp} [IsTrans β s] :
                                            WellFounded s ∀ (α : Type u) (r : ααProp), r ≺i sWellFounded r

                                            Properties of initial and principal segments #

                                            noncomputable def InitialSeg.ltOrEq {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [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
                                            Instances For
                                              theorem InitialSeg.ltOrEq_apply_left {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ≼i s) (g : r ≺i s) (a : α) :
                                              g.toRelEmbedding a = f a
                                              theorem InitialSeg.ltOrEq_apply_right {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ≼i s) (g : r ≃r s) (a : α) :
                                              g a = f a
                                              noncomputable def InitialSeg.leLT {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsWellOrder β s] [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
                                              Instances For
                                                @[simp]
                                                theorem InitialSeg.leLT_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) (a : α) :
                                                (f.leLT g).toRelEmbedding a = g.toRelEmbedding (f a)
                                                noncomputable def RelEmbedding.collapseF {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ↪r s) (a : α) :
                                                { b : β // ¬s (f a) b }

                                                Given an order embedding into a well order, collapse the order embedding by filling the gaps, to obtain an initial segment. Here, we construct the collapsed order embedding pointwise, but the proof of the fact that it is an initial segment will be given in collapse.

                                                Equations
                                                • f.collapseF = .fix fun (a : α) (IH : (y : α) → r y a{ b : β // ¬s (f y) b }) => let S := {b : β | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}; let_fun this := ; .min S ,
                                                Instances For
                                                  theorem RelEmbedding.collapseF.lt {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ↪r s) {a : α} {a' : α} :
                                                  r a' as (f.collapseF a') (f.collapseF a)
                                                  theorem RelEmbedding.collapseF.not_lt {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ↪r s) (a : α) {b : β} (h : ∀ (a' : α), r a' as (↑(f.collapseF a')) b) :
                                                  ¬s b (f.collapseF a)
                                                  noncomputable def RelEmbedding.collapse {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [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
                                                  • f.collapse = { toRelEmbedding := RelEmbedding.ofMonotone (fun (a : α) => (f.collapseF a)) , mem_range_of_rel' := }
                                                  Instances For
                                                    theorem RelEmbedding.collapse_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ↪r s) (a : α) :
                                                    f.collapse a = (f.collapseF a)
                                                    noncomputable def InitialSeg.total {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsWellOrder α r] [IsWellOrder β s] :
                                                    (r ≼i s) (s ≼i r)

                                                    For any two well orders, one is an initial segment of the other.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For