# Chains and flags #

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

## Main declarations #

• IsChain s: A chain s is a set of comparable elements.
• maxChain_spec: Hausdorff's Maximality Principle.
• Flag: The type of flags, aka maximal chains, of an order.

## 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} [] (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
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} [] [] {f : αβ} (hf : ) :
IsChain (fun (x x_1 : β) => x x_1) ()
theorem IsChain.lt_of_le {α : Type u_1} [] {s : Set α} (h : IsChain (fun (x x_1 : α) => x x_1) s) :
IsChain (fun (x x_1 : α) => x < x_1) 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 : ) :
theorem IsMaxChain.not_superChain {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (h : ) :
theorem IsMaxChain.bot_mem {α : Type u_1} {s : Set α} [LE α] [] (h : IsMaxChain (fun (x x_1 : α) => x x_1) s) :
theorem IsMaxChain.top_mem {α : Type u_1} {s : Set α} [LE α] [] (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
Instances For
theorem succChain_spec {α : Type u_1} {r : ααProp} {s : Set α} (h : ∃ (t : Set α), IsChain r s SuperChain r s t) :
SuperChain r s ()
theorem IsChain.succ {α : Type u_1} {r : ααProp} {s : Set α} (hs : IsChain r s) :
IsChain r ()
theorem IsChain.superChain_succChain {α : Type u_1} {r : ααProp} {s : Set α} (hs₁ : IsChain r s) (hs₂ : ¬) :
SuperChain r s ()
theorem subset_succChain {α : Type u_1} {r : ααProp} {s : Set α} :
s
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 : ) :
= c c =
theorem ChainClosure.isChain {α : Type u_1} {r : ααProp} {c : Set α} (hc : ) :
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 (x x_1 : α) => x x_1) self.carrier

By definition, a flag is a chain

• max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun (x x_1 : α) => x x_1) 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 (x x_1 : α) => x x_1) self.carrier

By definition, a flag is a chain

theorem Flag.max_chain' {α : Type u_3} [LE α] (self : Flag α) ⦃s : Set α :
IsChain (fun (x x_1 : α) => x x_1) 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 {α : 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 (x x_1 : α) => x x_1) s) (h₂ : ∀ ⦃s_1 : Set α⦄, IsChain (fun (x x_1 : α) => x x_1) 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 (x x_1 : α) => x x_1) s
theorem Flag.maxChain {α : Type u_1} [LE α] (s : Flag α) :
IsMaxChain (fun (x x_1 : α) => x x_1) s
theorem Flag.top_mem {α : Type u_1} [LE α] [] (s : Flag α) :
theorem Flag.bot_mem {α : Type u_1} [LE α] [] (s : Flag α) :
theorem Flag.le_or_le {α : Type u_1} [] {a : α} {b : α} (s : Flag α) (ha : a s) (hb : b s) :
a b b a
instance Flag.instOrderTopSubtypeMem {α : Type u_1} [] [] (s : Flag α) :
Equations
• s.instOrderTopSubtypeMem =
instance Flag.instOrderBotSubtypeMem {α : Type u_1} [] [] (s : Flag α) :
Equations
• s.instOrderBotSubtypeMem =
instance Flag.instBoundedOrderSubtypeMem {α : Type u_1} [] [] (s : Flag α) :
Equations
• s.instBoundedOrderSubtypeMem =
theorem Flag.chain_lt {α : Type u_1} [] (s : Flag α) :
IsChain (fun (x x_1 : α) => x < x_1) s
instance Flag.instLinearOrderSubtypeMemOfLeOfDecidableRelLt {α : Type u_1} [] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : α) => x < x_1] (s : Flag α) :
Equations
• s.instLinearOrderSubtypeMemOfLeOfDecidableRelLt = let __src := Subtype.partialOrder fun (x : α) => x s; LinearOrder.mk Subtype.decidableLE decidableEqOfDecidableLE Subtype.decidableLT
instance Flag.instUnique {α : Type u_1} [] :
Equations
• Flag.instUnique = { default := { carrier := Set.univ, Chain' := , max_chain' := }, uniq := }