Documentation

Mathlib.Order.Chain

Chains and flags #

This file defines chains for an arbitrary relation and flags for an order and proves Hausdorff's Maximality Principle.

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
  • IsChain r s = s.Pairwise fun (x y : α) => r x y r y x
Instances For
    def SuperChain {α : Type u_1} (r : ααProp) (s : Set α) (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
        theorem isChain_empty {α : Type u_1} {r : ααProp} :
        theorem Set.Subsingleton.isChain {α : Type u_1} {r : ααProp} {s : Set α} (hs : s.Subsingleton) :
        theorem IsChain.mono {α : Type u_1} {r : ααProp} {s : Set α} {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_univ_iff {α : Type u_1} {r : ααProp} :
        IsChain r Set.univ IsTrichotomous α r
        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 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 IsMaxChain.isChain {α : Type u_1} {r : ααProp} {s : Set α} (h : IsMaxChain r s) :
        theorem IsMaxChain.not_superChain {α : Type u_1} {r : ααProp} {s : Set α} {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) :
        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 α} :
          inductive ChainClosure {α : Type u_1} (r : ααProp) :
          Set αProp

          Predicate for whether a set is reachable from using SuccChain and ⋃₀.

          Instances For
            def maxChain {α : Type u_1} (r : ααProp) :
            Set α

            An explicit maximal chain. maxChain is taken to be the union of all sets in ChainClosure.

            Equations
            Instances For
              theorem chainClosure_empty {α : Type u_1} {r : ααProp} :
              theorem chainClosure_maxChain {α : Type u_1} {r : ααProp} :
              theorem ChainClosure.total {α : Type u_1} {r : ααProp} {c₁ : Set α} {c₂ : Set α} (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) :
              c₁ c₂ c₂ c₁
              theorem ChainClosure.succ_fixpoint {α : Type u_1} {r : ααProp} {c₁ : Set α} {c₂ : Set α} (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) (hc : SuccChain r c₂ = c₂) :
              c₁ c₂
              theorem ChainClosure.succ_fixpoint_iff {α : Type u_1} {r : ααProp} {c : Set α} (hc : ChainClosure r c) :
              theorem ChainClosure.isChain {α : Type u_1} {r : ααProp} {c : Set α} (hc : ChainClosure r c) :
              theorem maxChain_spec {α : Type u_1} {r : ααProp} :

              Hausdorff's maximality principle

              There exists a maximal totally ordered set of α. Note that we do not require α to be partially ordered by r.

              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
                theorem Flag.Chain' {α : Type u_3} [LE α] (self : Flag α) :
                IsChain (fun (x1 x2 : α) => x1 x2) self.carrier

                By definition, a flag is a chain

                theorem Flag.max_chain' {α : Type u_3} [LE α] (self : Flag α) ⦃s : Set α :
                IsChain (fun (x1 x2 : α) => x1 x2) sself.carrier sself.carrier = s

                By definition, a flag is a maximal chain

                instance Flag.instSetLike {α : Type u_1} [LE α] :
                SetLike (Flag α) α
                Equations
                • Flag.instSetLike = { coe := Flag.carrier, coe_injective' := }
                theorem Flag.ext_iff {α : Type u_1} [LE α] {s : Flag α} {t : Flag α} :
                s = t s = t
                theorem Flag.ext {α : Type u_1} [LE α] {s : Flag α} {t : Flag α} :
                s = ts = 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 α) :
                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.chain_lt {α : Type u_1} [PartialOrder α] (s : Flag α) :
                IsChain (fun (x1 x2 : α) => x1 < x2) s
                instance Flag.instLinearOrderSubtypeMemOfLeOfDecidableRelLt {α : Type u_1} [PartialOrder α] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 < x2] (s : Flag α) :
                Equations
                • s.instLinearOrderSubtypeMemOfLeOfDecidableRelLt = LinearOrder.mk Subtype.decidableLE decidableEqOfDecidableLE Subtype.decidableLT
                instance Flag.instUnique {α : Type u_1} [LinearOrder α] :
                Equations
                • Flag.instUnique = { default := { carrier := Set.univ, Chain' := , max_chain' := }, uniq := }