Documentation

Mathlib.Order.InitialSeg

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 #

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.

Initial segment embeddings #

structure InitialSeg {α : Type u_4} {β : Type u_5} (r : ααProp) (s : ββProp) extends r ↪r s :
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 Set.range is a lower set. 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 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.

    Equations
      Instances For

        An InitialSeg between the < relations of two types.

        Equations
          Instances For
            instance InitialSeg.instCoeRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
            Coe (InitialSeg r s) (r ↪r s)
            Equations
              instance InitialSeg.instFunLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
              FunLike (InitialSeg r s) α β
              Equations
                instance InitialSeg.instEmbeddingLike {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                instance InitialSeg.instRelHomClass {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                def InitialSeg.toOrderEmbedding {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                α ↪o β

                An initial segment embedding between the < relations of two partial orders is an order embedding.

                Equations
                  Instances For
                    @[simp]
                    theorem InitialSeg.toOrderEmbedding_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (x : α) :
                    @[simp]
                    theorem InitialSeg.coe_toOrderEmbedding {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                    instance InitialSeg.instOrderHomClassLt {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] :
                    OrderHomClass (InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) α β
                    theorem InitialSeg.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f g : InitialSeg r s} (h : ∀ (x : α), f x = g x) :
                    f = g
                    theorem InitialSeg.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {f g : InitialSeg r s} :
                    f = g ∀ (x : α), f x = g x
                    @[simp]
                    theorem InitialSeg.coe_coe_fn {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : InitialSeg r s) :
                    f.toRelEmbedding = f
                    theorem InitialSeg.mem_range_of_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : InitialSeg r s) {a : α} {b : β} :
                    s b (f a)b Set.range f
                    theorem InitialSeg.map_rel_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {a b : α} (f : InitialSeg r s) :
                    s (f a) (f b) r a b
                    theorem InitialSeg.inj {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : InitialSeg r s) {a b : α} :
                    f a = f b a = b
                    theorem InitialSeg.exists_eq_iff_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : InitialSeg r s) {a : α} {b : β} :
                    s b (f a) ∃ (a' : α), f a' = b r a' a
                    def RelIso.toInitialSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :

                    A relation isomorphism is an initial segment embedding

                    Equations
                      Instances For
                        @[simp]
                        theorem RelIso.toInitialSeg_toFun {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) (a : α) :
                        f.toInitialSeg a = f a
                        @[deprecated RelIso.toInitialSeg (since := "2024-10-22")]
                        def InitialSeg.ofIso {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ≃r s) :

                        Alias of RelIso.toInitialSeg.


                        A relation isomorphism is an initial segment embedding

                        Equations
                          Instances For
                            def InitialSeg.refl {α : Type u_1} (r : ααProp) :

                            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 : InitialSeg r s) (g : InitialSeg s t) :

                                  Composition of functions shows that ≼i is transitive

                                  Equations
                                    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 : InitialSeg r s) (g : InitialSeg s 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] :
                                      instance InitialSeg.instSubsingletonOfIsWellOrder {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] :

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

                                      theorem InitialSeg.eq {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f g : InitialSeg r s) (a : α) :
                                      f a = g a
                                      theorem InitialSeg.eq_relIso {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : InitialSeg r s) (g : r ≃r s) (a : α) :
                                      g a = f a
                                      def InitialSeg.antisymm {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : InitialSeg r s) (g : InitialSeg s r) :
                                      r ≃r s

                                      If we have order embeddings between α and β whose ranges are initial segments, and β is a well order, then α and β are order-isomorphic.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem InitialSeg.antisymm_toFun {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : InitialSeg r s) (g : InitialSeg s 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 : InitialSeg r s) (g : InitialSeg s r) :
                                          theorem InitialSeg.eq_or_principal {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : InitialSeg r s) :
                                          Function.Surjective f ∃ (b : β), ∀ (x : β), x Set.range f s x b

                                          An initial segment embedding is either an isomorphism, or a principal segment embedding.

                                          See also InitialSeg.ltOrEq.

                                          def InitialSeg.codRestrict {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : InitialSeg r s) (H : ∀ (a : α), f a p) :
                                          InitialSeg r (Subrel s fun (x : β) => x 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 : InitialSeg r s) (H : ∀ (a : α), f a p) (a : α) :
                                              (codRestrict p f H) a = f a,
                                              def InitialSeg.ofIsEmpty {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsEmpty α] :

                                              Initial segment embedding 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
                                                    Instances For
                                                      @[simp]
                                                      theorem InitialSeg.leAdd_apply {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (a : α) :
                                                      (leAdd r s) a = Sum.inl a
                                                      theorem InitialSeg.acc {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : InitialSeg r s) (a : α) :
                                                      Acc r a Acc s (f a)

                                                      Principal segments #

                                                      structure PrincipalSeg {α : Type u_4} {β : Type u_5} (r : ααProp) (s : ββProp) extends r ↪r s :
                                                      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 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.

                                                      Instances For

                                                        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.

                                                        Equations
                                                          Instances For

                                                            A PrincipalSeg between the < relations of two types.

                                                            Equations
                                                              Instances For
                                                                instance PrincipalSeg.instCoeOutRelEmbedding {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                                                Equations
                                                                  instance PrincipalSeg.instCoeFunForall {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} :
                                                                  CoeFun (PrincipalSeg r s) fun (x : PrincipalSeg r s) => αβ
                                                                  Equations
                                                                    theorem PrincipalSeg.toRelEmbedding_injective {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsIrrefl β s] [IsTrichotomous β s] :
                                                                    @[simp]
                                                                    theorem PrincipalSeg.toRelEmbedding_inj {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsIrrefl β s] [IsTrichotomous β s] {f g : PrincipalSeg r s} :
                                                                    theorem PrincipalSeg.ext {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsIrrefl β s] [IsTrichotomous β s] {f g : PrincipalSeg r s} (h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x) :
                                                                    f = g
                                                                    theorem PrincipalSeg.ext_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsIrrefl β s] [IsTrichotomous β s] {f g : PrincipalSeg r s} :
                                                                    f = g ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
                                                                    @[simp]
                                                                    theorem PrincipalSeg.coe_fn_mk {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : r ↪r s) (t : β) (o : ∀ (b : β), b Set.range f s b t) :
                                                                    { toRelEmbedding := f, top := t, mem_range_iff_rel' := o }.toRelEmbedding = f
                                                                    theorem PrincipalSeg.mem_range_iff_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : PrincipalSeg r s) {b : β} :
                                                                    theorem PrincipalSeg.lt_top {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : PrincipalSeg r s) (a : α) :
                                                                    theorem PrincipalSeg.mem_range_of_rel_top {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : PrincipalSeg r s) {b : β} (h : s b f.top) :
                                                                    theorem PrincipalSeg.mem_range_of_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : PrincipalSeg r s) {a : α} {b : β} (h : s b (f.toRelEmbedding a)) :
                                                                    theorem PrincipalSeg.surjOn {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : PrincipalSeg r s) :
                                                                    instance PrincipalSeg.hasCoeInitialSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] :

                                                                    A principal segment embedding is in particular an initial segment embedding.

                                                                    Equations
                                                                      theorem PrincipalSeg.coe_coe_fn' {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : PrincipalSeg r s) :
                                                                      { toRelEmbedding := f.toRelEmbedding, mem_range_of_rel' := } = f.toRelEmbedding
                                                                      theorem InitialSeg.eq_principalSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : InitialSeg r s) (g : PrincipalSeg r s) (a : α) :
                                                                      theorem PrincipalSeg.exists_eq_iff_rel {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsTrans β s] (f : PrincipalSeg r s) {a : α} {b : β} :
                                                                      s b (f.toRelEmbedding a) ∃ (a' : α), f.toRelEmbedding a' = b r a' a
                                                                      noncomputable def InitialSeg.toPrincipalSeg {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : InitialSeg r s) (hf : ¬Function.Surjective f) :

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

                                                                      Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem InitialSeg.toPrincipalSeg_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : InitialSeg r s) (hf : ¬Function.Surjective f) (x : α) :
                                                                          theorem PrincipalSeg.irrefl {α : Type u_1} {r : ααProp} [IsWellOrder α r] (f : PrincipalSeg r r) :
                                                                          instance PrincipalSeg.instIsEmptyOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                                                                          def PrincipalSeg.transInitial {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : PrincipalSeg r s) (g : InitialSeg s t) :

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

                                                                          Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem PrincipalSeg.transInitial_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : PrincipalSeg r s) (g : InitialSeg s t) (a : α) :
                                                                              @[simp]
                                                                              theorem PrincipalSeg.transInitial_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : PrincipalSeg r s) (g : InitialSeg s t) :
                                                                              (f.transInitial 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 : PrincipalSeg r s) (g : PrincipalSeg s t) :

                                                                              Composition of two principal segment embeddings as a principal segment embedding

                                                                              Equations
                                                                                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 : PrincipalSeg r s) (g : PrincipalSeg s t) (a : α) :
                                                                                  @[simp]
                                                                                  theorem PrincipalSeg.trans_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsTrans γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t) :
                                                                                  def PrincipalSeg.relIsoTrans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≃r s) (g : PrincipalSeg s t) :

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

                                                                                  Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem PrincipalSeg.relIsoTrans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≃r s) (g : PrincipalSeg s t) (a : α) :
                                                                                      @[simp]
                                                                                      theorem PrincipalSeg.relIsoTrans_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : r ≃r s) (g : PrincipalSeg s t) :
                                                                                      def PrincipalSeg.transRelIso {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : PrincipalSeg r s) (g : s ≃r t) :

                                                                                      Composition of a principal segment embedding with a relation isomorphism, as a principal segment embedding

                                                                                      Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem PrincipalSeg.transRelIso_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : PrincipalSeg r s) (g : s ≃r t) (a : α) :
                                                                                          @[simp]
                                                                                          theorem PrincipalSeg.transRelIso_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} (f : PrincipalSeg r s) (g : s ≃r t) :
                                                                                          (f.transRelIso g).top = g f.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.

                                                                                          theorem PrincipalSeg.eq {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f g : PrincipalSeg r s) (a : α) :
                                                                                          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 : PrincipalSeg r t) (g : PrincipalSeg s t) :
                                                                                          f.top = g.top
                                                                                          theorem PrincipalSeg.top_rel_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsWellOrder γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t) (h : PrincipalSeg r t) :
                                                                                          t h.top g.top
                                                                                          def PrincipalSeg.ofElement {α : Type u_4} (r : ααProp) (a : α) :
                                                                                          PrincipalSeg (Subrel r fun (x : α) => r x a) r

                                                                                          Any element of a well order yields a principal segment.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem PrincipalSeg.ofElement_top {α : Type u_4} (r : ααProp) (a : α) :
                                                                                              (ofElement r a).top = a
                                                                                              @[simp]
                                                                                              theorem PrincipalSeg.ofElement_toFun {α : Type u_4} (r : ααProp) (a : α) (self : { x : α // r x a }) :
                                                                                              (ofElement r a).toFun self = self
                                                                                              @[simp]
                                                                                              theorem PrincipalSeg.ofElement_apply {α : Type u_4} (r : ααProp) (a : α) (b : { x : α // r x a }) :
                                                                                              noncomputable def PrincipalSeg.subrelIso {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : PrincipalSeg r s) :
                                                                                              (Subrel s fun (x : β) => s x 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.subrelIso_symm_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : PrincipalSeg r s) (a✝ : α) :
                                                                                                  @[simp]
                                                                                                  theorem PrincipalSeg.apply_subrelIso {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : PrincipalSeg r s) (b : { b : β // s b f.top }) :
                                                                                                  @[simp]
                                                                                                  theorem PrincipalSeg.subrelIso_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (f : PrincipalSeg r s) (a : α) :
                                                                                                  def PrincipalSeg.codRestrict {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : PrincipalSeg r s) (H : ∀ (a : α), f.toRelEmbedding a p) (H₂ : f.top p) :
                                                                                                  PrincipalSeg r (Subrel s fun (x : β) => x p)

                                                                                                  Restrict the codomain of a principal segment embedding.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem PrincipalSeg.codRestrict_apply {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : PrincipalSeg r s) (H : ∀ (a : α), f.toRelEmbedding a p) (H₂ : f.top p) (a : α) :
                                                                                                      @[simp]
                                                                                                      theorem PrincipalSeg.codRestrict_top {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (p : Set β) (f : PrincipalSeg r s) (H : ∀ (a : α), f.toRelEmbedding a p) (H₂ : f.top p) :
                                                                                                      (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) :

                                                                                                      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) :
                                                                                                          (ofIsEmpty r H).top = b
                                                                                                          @[reducible, inline]

                                                                                                          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 : PrincipalSeg r s) (a : α) :
                                                                                                              theorem wellFounded_iff_principalSeg {β : Type u} {s : ββProp} [IsTrans β s] :
                                                                                                              WellFounded s ∀ (α : Type u) (r : ααProp) (x : PrincipalSeg r s), WellFounded r

                                                                                                              Properties of initial and principal segments #

                                                                                                              noncomputable def InitialSeg.principalSumRelIso {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : InitialSeg r s) :

                                                                                                              Every initial segment embedding into a well order can be turned into an isomorphism if surjective, or into a principal segment embedding if not.

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  noncomputable def InitialSeg.transPrincipal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsWellOrder β s] [IsTrans γ t] (f : InitialSeg r s) (g : PrincipalSeg s t) :

                                                                                                                  Composition of an initial segment embedding and a principal segment embedding as a principal segment embedding

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      @[simp]
                                                                                                                      theorem InitialSeg.transPrincipal_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {s : ββProp} {t : γγProp} [IsWellOrder β s] [IsTrans γ t] (f : InitialSeg r s) (g : PrincipalSeg s t) (a : α) :
                                                                                                                      noncomputable def RelEmbedding.collapse {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} [IsWellOrder β s] (f : r ↪r s) :

                                                                                                                      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.

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          noncomputable def InitialSeg.total {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsWellOrder α r] [IsWellOrder β s] :

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

                                                                                                                          Equations
                                                                                                                            Instances For

                                                                                                                              Initial or principal segments with < #

                                                                                                                              def OrderIso.toInitialSeg {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :
                                                                                                                              InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2

                                                                                                                              An order isomorphism is an initial segment

                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  @[simp]
                                                                                                                                  theorem OrderIso.toInitialSeg_toFun {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
                                                                                                                                  f.toInitialSeg a = f a
                                                                                                                                  theorem InitialSeg.mem_range_of_le {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [LT α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (h : b f a) :
                                                                                                                                  b Set.range f
                                                                                                                                  theorem InitialSeg.isLowerSet_range {α : Type u_1} {β : Type u_2} [PartialOrder β] [LT α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  @[simp]
                                                                                                                                  theorem InitialSeg.le_iff_le {α : Type u_1} {β : Type u_2} [PartialOrder β] {a a' : α} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  f a f a' a a'
                                                                                                                                  @[simp]
                                                                                                                                  theorem InitialSeg.lt_iff_lt {α : Type u_1} {β : Type u_2} [PartialOrder β] {a a' : α} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  f a < f a' a < a'
                                                                                                                                  theorem InitialSeg.monotone {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  theorem InitialSeg.strictMono {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  @[simp]
                                                                                                                                  theorem InitialSeg.isMin_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  IsMin (f a) IsMin a
                                                                                                                                  theorem InitialSeg.map_isMin {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  IsMin aIsMin (f a)

                                                                                                                                  Alias of the reverse direction of InitialSeg.isMin_apply_iff.

                                                                                                                                  @[simp]
                                                                                                                                  theorem InitialSeg.map_bot {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] [OrderBot α] [OrderBot β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  theorem InitialSeg.image_Iio {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) :
                                                                                                                                  f '' Set.Iio a = Set.Iio (f a)
                                                                                                                                  theorem InitialSeg.le_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  b f a ca, f c = b
                                                                                                                                  theorem InitialSeg.lt_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [PartialOrder α] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  b < f a a' < a, f a' = b
                                                                                                                                  theorem PrincipalSeg.mem_range_of_le {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [LT α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (h : b f.toRelEmbedding a) :
                                                                                                                                  theorem PrincipalSeg.isLowerSet_range {α : Type u_1} {β : Type u_2} [PartialOrder β] [LT α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  @[simp]
                                                                                                                                  theorem PrincipalSeg.le_iff_le {α : Type u_1} {β : Type u_2} [PartialOrder β] {a a' : α} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  @[simp]
                                                                                                                                  theorem PrincipalSeg.lt_iff_lt {α : Type u_1} {β : Type u_2} [PartialOrder β] {a a' : α} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  theorem PrincipalSeg.monotone {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  theorem PrincipalSeg.strictMono {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  @[simp]
                                                                                                                                  theorem PrincipalSeg.isMin_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  theorem PrincipalSeg.map_isMin {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :

                                                                                                                                  Alias of the reverse direction of PrincipalSeg.isMin_apply_iff.

                                                                                                                                  @[simp]
                                                                                                                                  theorem PrincipalSeg.map_bot {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] [OrderBot α] [OrderBot β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  theorem PrincipalSeg.image_Iio {α : Type u_1} {β : Type u_2} [PartialOrder β] [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) :
                                                                                                                                  theorem PrincipalSeg.le_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  b f.toRelEmbedding a ca, f.toRelEmbedding c = b
                                                                                                                                  theorem PrincipalSeg.lt_apply_iff {α : Type u_1} {β : Type u_2} [PartialOrder β] {a : α} {b : β} [PartialOrder α] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
                                                                                                                                  b < f.toRelEmbedding a a' < a, f.toRelEmbedding a' = b