Documentation

Mathlib.Order.Preorder.Chain

Chains and flags #

This file defines chains for an arbitrary relation and flags for an order.

Main declarations #

Notes #

Originally ported from Isabelle/HOL. The original file was written by Jacques D. Fleuriot, Tobias Nipkow, Christian Sternagel.

Chains #

def IsChain {α : Type u_1} (r : ααProp) (s : Set α) :

A chain is a set s satisfying x ≺ y ∨ x = y ∨ y ≺ x for all x y ∈ s.

Equations
    Instances For
      def SuperChain {α : Type u_1} (r : ααProp) (s t : Set α) :

      SuperChain s t means that t is a chain that strictly includes s.

      Equations
        Instances For
          def IsMaxChain {α : Type u_1} (r : ααProp) (s : Set α) :

          A chain s is a maximal chain if there does not exists a chain strictly including s.

          Equations
            Instances For
              @[simp]
              theorem IsChain.empty {α : Type u_1} {r : ααProp} :
              @[simp]
              theorem IsChain.singleton {α : Type u_1} {r : ααProp} {a : α} :
              @[deprecated IsChain.empty (since := "2024-11-25")]
              theorem isChain_empty {α : Type u_1} {r : ααProp} :

              Alias of IsChain.empty.

              theorem Set.Subsingleton.isChain {α : Type u_1} {r : ααProp} {s : Set α} (hs : s.Subsingleton) :
              theorem IsChain.mono {α : Type u_1} {r : ααProp} {s t : Set α} :
              s tIsChain r tIsChain r s
              theorem IsChain.mono_rel {α : Type u_1} {r : ααProp} {s : Set α} {r' : ααProp} (h : IsChain r s) (h_imp : ∀ (x y : α), r x yr' x y) :
              IsChain r' s
              theorem IsChain.symm {α : Type u_1} {r : ααProp} {s : Set α} (h : IsChain r s) :

              This can be used to turn IsChain (≥) into IsChain (≤) and vice-versa.

              theorem isChain_of_trichotomous {α : Type u_1} {r : ααProp} [IsTrichotomous α r] (s : Set α) :
              theorem IsChain.insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : IsChain r s) (ha : bs, a br a b r b a) :
              IsChain r (insert a s)
              theorem IsChain.pair {α : Type u_1} {r : ααProp} {a b : α} (h : r a b) :
              theorem isChain_univ_iff {α : Type u_1} {r : ααProp} :
              theorem IsChain.image {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) (f : αβ) (h : ∀ (x y : α), r x ys (f x) (f y)) {c : Set α} (hrc : IsChain r c) :
              IsChain s (f '' c)
              theorem isChain_union {α : Type u_1} {r : ααProp} {s t : Set α} :
              IsChain r (s t) IsChain r s IsChain r t as, bt, a br a b r b a
              theorem Monotone.isChain_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {f : αβ} (hf : Monotone f) (hs : IsChain (fun (x1 x2 : α) => x1 x2) s) :
              IsChain (fun (x1 x2 : β) => x1 x2) (f '' s)
              theorem Monotone.isChain_range {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : αβ} (hf : Monotone f) :
              IsChain (fun (x1 x2 : β) => x1 x2) (Set.range f)
              theorem IsChain.lt_of_le {α : Type u_1} [PartialOrder α] {s : Set α} (h : IsChain (fun (x1 x2 : α) => x1 x2) s) :
              IsChain (fun (x1 x2 : α) => x1 < x2) s
              theorem IsChain.total {α : Type u_1} {r : ααProp} {s : Set α} {x y : α} [IsRefl α r] (h : IsChain r s) (hx : x s) (hy : y s) :
              r x y r y x
              theorem IsChain.directedOn {α : Type u_1} {r : ααProp} {s : Set α} [IsRefl α r] (H : IsChain r s) :
              theorem IsChain.directed {α : Type u_1} {β : Type u_2} {r : ααProp} [IsRefl α r] {f : βα} {c : Set β} (h : IsChain (f ⁻¹'o r) c) :
              Directed r fun (x : { a : β // a c }) => f x
              theorem IsChain.exists3 {α : Type u_1} {r : ααProp} {s : Set α} [IsRefl α r] (hchain : IsChain r s) [IsTrans α r] {a b c : α} (mem1 : a s) (mem2 : b s) (mem3 : c s) :
              ∃ (z : α) (_ : z s), r a z r b z r c z
              theorem IsChain.le_of_not_lt {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 x2) s) {x y : α} (hx : x s) (hy : y s) (h : ¬x < y) :
              y x
              theorem IsChain.not_lt {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 x2) s) {x y : α} (hx : x s) (hy : y s) :
              ¬x < y y x
              theorem IsChain.lt_of_not_le {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 x2) s) {x y : α} (hx : x s) (hy : y s) (h : ¬x y) :
              y < x
              theorem IsChain.not_le {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 x2) s) {x y : α} (hx : x s) (hy : y s) :
              ¬x y y < x
              theorem IsMaxChain.isChain {α : Type u_1} {r : ααProp} {s : Set α} (h : IsMaxChain r s) :
              theorem IsMaxChain.not_superChain {α : Type u_1} {r : ααProp} {s t : Set α} (h : IsMaxChain r s) :
              theorem IsMaxChain.bot_mem {α : Type u_1} {s : Set α} [LE α] [OrderBot α] (h : IsMaxChain (fun (x1 x2 : α) => x1 x2) s) :
              theorem IsMaxChain.top_mem {α : Type u_1} {s : Set α} [LE α] [OrderTop α] (h : IsMaxChain (fun (x1 x2 : α) => x1 x2) s) :
              theorem IsMaxChain.image {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (e : r ≃r s) {c : Set α} (hc : IsMaxChain r c) :
              IsMaxChain s (e '' c)
              def SuccChain {α : Type u_1} (r : ααProp) (s : Set α) :
              Set α

              Given a set s, if there exists a chain t strictly including s, then SuccChain s is one of these chains. Otherwise it is s.

              Equations
                Instances For
                  theorem succChain_spec {α : Type u_1} {r : ααProp} {s : Set α} (h : ∃ (t : Set α), IsChain r s SuperChain r s t) :
                  theorem IsChain.succ {α : Type u_1} {r : ααProp} {s : Set α} (hs : IsChain r s) :
                  theorem IsChain.superChain_succChain {α : Type u_1} {r : ααProp} {s : Set α} (hs₁ : IsChain r s) (hs₂ : ¬IsMaxChain r s) :
                  theorem subset_succChain {α : Type u_1} {r : ααProp} {s : Set α} :

                  Flags #

                  structure Flag (α : Type u_3) [LE α] :
                  Type u_3

                  The type of flags, aka maximal chains, of an order.

                  • carrier : Set α

                    The carrier of a flag is the underlying set.

                  • Chain' : IsChain (fun (x1 x2 : α) => x1 x2) self.carrier

                    By definition, a flag is a chain

                  • max_chain' s : Set α : IsChain (fun (x1 x2 : α) => x1 x2) sself.carrier sself.carrier = s

                    By definition, a flag is a maximal chain

                  Instances For
                    instance Flag.instSetLike {α : Type u_1} [LE α] :
                    SetLike (Flag α) α
                    Equations
                      theorem Flag.ext {α : Type u_1} [LE α] {s t : Flag α} :
                      s = ts = t
                      theorem Flag.ext_iff {α : Type u_1} [LE α] {s t : Flag α} :
                      s = t s = t
                      theorem Flag.mem_coe_iff {α : Type u_1} [LE α] {s : Flag α} {a : α} :
                      a s a s
                      @[simp]
                      theorem Flag.coe_mk {α : Type u_1} [LE α] (s : Set α) (h₁ : IsChain (fun (x1 x2 : α) => x1 x2) s) (h₂ : ∀ ⦃s_1 : Set α⦄, IsChain (fun (x1 x2 : α) => x1 x2) s_1s s_1s = s_1) :
                      { carrier := s, Chain' := h₁, max_chain' := h₂ } = s
                      @[simp]
                      theorem Flag.mk_coe {α : Type u_1} [LE α] (s : Flag α) :
                      { carrier := s, Chain' := , max_chain' := } = s
                      theorem Flag.chain_le {α : Type u_1} [LE α] (s : Flag α) :
                      IsChain (fun (x1 x2 : α) => x1 x2) s
                      theorem Flag.maxChain {α : Type u_1} [LE α] (s : Flag α) :
                      IsMaxChain (fun (x1 x2 : α) => x1 x2) s
                      theorem Flag.top_mem {α : Type u_1} [LE α] [OrderTop α] (s : Flag α) :
                      theorem Flag.bot_mem {α : Type u_1} [LE α] [OrderBot α] (s : Flag α) :
                      def Flag.ofIsMaxChain {α : Type u_1} [LE α] (c : Set α) (hc : IsMaxChain (fun (x1 x2 : α) => x1 x2) c) :
                      Flag α

                      Reinterpret a maximal chain as a flag.

                      Equations
                        Instances For
                          @[simp]
                          theorem Flag.coe_ofIsMaxChain {α : Type u_1} [LE α] (c : Set α) (hc : IsMaxChain (fun (x1 x2 : α) => x1 x2) c) :
                          (ofIsMaxChain c hc) = c
                          theorem Flag.le_or_le {α : Type u_1} [Preorder α] {a b : α} (s : Flag α) (ha : a s) (hb : b s) :
                          a b b a
                          instance Flag.instOrderTopSubtypeMem {α : Type u_1} [Preorder α] [OrderTop α] (s : Flag α) :
                          Equations
                            instance Flag.instOrderBotSubtypeMem {α : Type u_1} [Preorder α] [OrderBot α] (s : Flag α) :
                            Equations
                              instance Flag.instBoundedOrderSubtypeMem {α : Type u_1} [Preorder α] [BoundedOrder α] (s : Flag α) :
                              Equations
                                theorem Flag.mem_iff_forall_le_or_ge {α : Type u_1} [Preorder α] {a : α} {s : Flag α} :
                                a s ∀ ⦃b : α⦄, b sa b b a
                                def Flag.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) :
                                Flag α Flag β

                                Flags are preserved under order isomorphisms.

                                Equations
                                  Instances For
                                    @[simp]
                                    theorem Flag.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) (s : Flag α) :
                                    ((map e) s) = e '' s
                                    @[simp]
                                    theorem Flag.symm_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) :
                                    (map e).symm = map e.symm
                                    theorem Flag.chain_lt {α : Type u_1} [PartialOrder α] (s : Flag α) :
                                    IsChain (fun (x1 x2 : α) => x1 < x2) s
                                    instance Flag.instUnique {α : Type u_1} [LinearOrder α] :
                                    Equations