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≺ y ∨ x = y ∨ y ≺ x∨ x = y ∨ y ≺ x∨ y ≺ x≺ x for all x y ∈ s∈ s.

Equations
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
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
theorem isChain_empty {α : Type u_1} {r : ααProp} :
theorem Set.Subsingleton.isChain {α : Type u_1} {r : ααProp} {s : Set α} (hs : Set.Subsingleton s) :
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} [inst : IsTrichotomous α r] (s : Set α) :
theorem IsChain.insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : IsChain r s) (ha : ∀ (b : α), b sa 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 IsChain.total {α : Type u_1} {r : ααProp} {s : Set α} {x : α} {y : α} [inst : 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 α} [inst : IsRefl α r] (H : IsChain r s) :
theorem IsChain.directed {α : Type u_2} {β : Type u_1} {r : ααProp} [inst : IsRefl α r] {f : βα} {c : Set β} (h : IsChain (f ⁻¹'o r) c) :
Directed r fun x => f x
theorem IsChain.exists3 {α : Type u_1} {r : ααProp} {s : Set α} [inst : IsRefl α r] (hchain : IsChain r s) [inst : IsTrans α r] {a : α} {b : α} {c : α} (mem1 : a s) (mem2 : b s) (mem3 : c s) :
z x, 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 α} [inst : LE α] [inst : OrderBot α] (h : IsMaxChain (fun x x_1 => x x_1) s) :
theorem IsMaxChain.top_mem {α : Type u_1} {s : Set α} [inst : LE α] [inst : OrderTop α] (h : IsMaxChain (fun x x_1 => x x_1) 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
theorem succChain_spec {α : Type u_1} {r : ααProp} {s : Set α} (h : t, 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
    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_1) [inst : LE α] :
    Type u_1
    • The carrier of a flag is the underlying set.

      carrier : Set α
    • By definition, a flag is a chain

      Chain' : IsChain (fun x x_1 => x x_1) carrier
    • By definition, a flag is a maximal chain

      max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x x_1) scarrier scarrier = s

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

    Instances For
      instance Flag.instSetLikeFlag {α : Type u_1} [inst : LE α] :
      SetLike (Flag α) α
      Equations
      • Flag.instSetLikeFlag = { coe := Flag.carrier, coe_injective' := (_ : ∀ (s t : Flag α), s.carrier = t.carriers = t) }
      theorem Flag.ext {α : Type u_1} [inst : LE α] {s : Flag α} {t : Flag α} :
      s = ts = t
      theorem Flag.mem_coe_iff {α : Type u_1} [inst : LE α] {s : Flag α} {a : α} :
      a s a s
      @[simp]
      theorem Flag.coe_mk {α : Type u_1} [inst : LE α] (s : Set α) (h₁ : IsChain (fun x x_1 => x x_1) s) (h₂ : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x x_1) ss ss = s) :
      { carrier := s, Chain' := h₁, max_chain' := h₂ } = s
      @[simp]
      theorem Flag.mk_coe {α : Type u_1} [inst : LE α] (s : Flag α) :
      { carrier := s, Chain' := (_ : IsChain (fun x x_1 => x x_1) s.carrier), max_chain' := (_ : ∀ ⦃s : Set α⦄, IsChain (fun x x_1 => x x_1) ss.carrier ss.carrier = s) } = s
      theorem Flag.chain_le {α : Type u_1} [inst : LE α] (s : Flag α) :
      IsChain (fun x x_1 => x x_1) s
      theorem Flag.maxChain {α : Type u_1} [inst : LE α] (s : Flag α) :
      IsMaxChain (fun x x_1 => x x_1) s
      theorem Flag.top_mem {α : Type u_1} [inst : LE α] [inst : OrderTop α] (s : Flag α) :
      theorem Flag.bot_mem {α : Type u_1} [inst : LE α] [inst : OrderBot α] (s : Flag α) :
      theorem Flag.le_or_le {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (s : Flag α) (ha : a s) (hb : b s) :
      a b b a
      theorem Flag.chain_lt {α : Type u_1} [inst : PartialOrder α] (s : Flag α) :
      IsChain (fun x x_1 => x < x_1) s
      instance Flag.instLinearOrderSubtypeMemFlagToLEToPreorderInstMembershipInstSetLikeFlag {α : Type u_1} [inst : PartialOrder α] [inst : DecidableRel fun x x_1 => x x_1] [inst : DecidableRel fun x x_1 => x < x_1] (s : Flag α) :
      LinearOrder { x // x s }
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.