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 #

source

ink

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

Prop

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

IsChain r s = Set.Pairwise s fun x y => r x y ∨ r y x

source

ink

def SuperChain {α : Type u_1} (r : α → α → Prop) (s : Set α) (t : Set α) :

Prop

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

Equations

SuperChain r s t = (IsChain r t ∧ s ⊂ t)

source

ink

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

Prop

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

Equations

IsMaxChain r s = (IsChain r s ∧ ∀ ⦃t : Set α⦄, IsChain r t → s ⊆ t → s = t)

source

ink

theorem isChain_empty {α : Type u_1} {r : α → α → Prop} :

IsChain r ∅

source

ink

theorem Set.Subsingleton.isChain {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : Set.Subsingleton s) :

IsChain r s

source

ink

theorem IsChain.mono {α : Type u_1} {r : α → α → Prop} {s : Set α} {t : Set α} :

s ⊆ t → IsChain r t → IsChain r s

source

ink

theorem IsChain.mono_rel {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop} (h : IsChain r s) (h_imp : (x y : α) → r x y → r' x y) :

IsChain r' s

source

ink

theorem IsChain.symm {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsChain r s) :

IsChain (flip r) s

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

source

ink

theorem isChain_of_trichotomous {α : Type u_1} {r : α → α → Prop} [inst : IsTrichotomous α r] (s : Set α) :

IsChain r s

source

ink

theorem IsChain.insert {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (hs : IsChain r s) (ha : ∀ (b : α), b ∈ s → a ≠ b → r a b ∨ r b a) :

IsChain r (insert a s)

source

ink

theorem isChain_univ_iff {α : Type u_1} {r : α → α → Prop} :

IsChain r Set.univ ↔ IsTrichotomous α r

source

ink

theorem IsChain.image {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (f : α → β) (h : (x y : α) → r x y → s (f x) (f y)) {c : Set α} (hrc : IsChain r c) :

IsChain s (f '' c)

source

ink

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

source

ink

theorem IsChain.directedOn {α : Type u_1} {r : α → α → Prop} {s : Set α} [inst : IsRefl α r] (H : IsChain r s) :

DirectedOn r s

source

ink

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

source

ink

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

source

ink

theorem IsMaxChain.isChain {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) :

IsChain r s

source

ink

theorem IsMaxChain.not_superChain {α : Type u_1} {r : α → α → Prop} {s : Set α} {t : Set α} (h : IsMaxChain r s) :

¬SuperChain r s t

source

ink

theorem IsMaxChain.bot_mem {α : Type u_1} {s : Set α} [inst : LE α] [inst : OrderBot α] (h : IsMaxChain (fun x x_1 => x ≤ x_1) s) :

⊥ ∈ s

source

ink

theorem IsMaxChain.top_mem {α : Type u_1} {s : Set α} [inst : LE α] [inst : OrderTop α] (h : IsMaxChain (fun x x_1 => x ≤ x_1) s) :

⊤ ∈ s

source

ink

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

SuccChain r s = if h : ∃ t, IsChain r s ∧ SuperChain r s t then Classical.choose h else s

source

ink

theorem succChain_spec {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : ∃ t, IsChain r s ∧ SuperChain r s t) :

SuperChain r s (SuccChain r s)

source

ink

theorem IsChain.succ {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsChain r s) :

IsChain r (SuccChain r s)

source

ink

theorem IsChain.superChain_succChain {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs₁ : IsChain r s) (hs₂ : ¬IsMaxChain r s) :

SuperChain r s (SuccChain r s)

source

ink

theorem subset_succChain {α : Type u_1} {r : α → α → Prop} {s : Set α} :

s ⊆ SuccChain r s

source

ink

inductive ChainClosure {α : Type u_1} (r : α → α → Prop) :

Set α → Prop

succ: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, ChainClosure r s → ChainClosure r (SuccChain r s)
union: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set (Set α)}, (∀ (a : Set α), a ∈ s → ChainClosure r a) → ChainClosure r (⋃₀ s)

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

Instances For

source

ink

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

maxChain r = ⋃₀ setOf (ChainClosure r)

source

ink

theorem chainClosure_empty {α : Type u_1} {r : α → α → Prop} :

ChainClosure r ∅

source

ink

theorem chainClosure_maxChain {α : Type u_1} {r : α → α → Prop} :

ChainClosure r (maxChain r)

source

ink

theorem ChainClosure.total {α : Type u_1} {r : α → α → Prop} {c₁ : Set α} {c₂ : Set α} (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) :

c₁ ⊆ c₂ ∨ c₂ ⊆ c₁

source

ink

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₂

source

ink

theorem ChainClosure.succ_fixpoint_iff {α : Type u_1} {r : α → α → Prop} {c : Set α} (hc : ChainClosure r c) :

SuccChain r c = c ↔ c = maxChain r

source

ink

theorem ChainClosure.isChain {α : Type u_1} {r : α → α → Prop} {c : Set α} (hc : ChainClosure r c) :

IsChain r c

source

ink

theorem maxChain_spec {α : Type u_1} {r : α → α → Prop} :

IsMaxChain r (maxChain r)

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 #

source

ink

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) s → carrier ⊆ s → carrier = s

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

Instances For

source

ink

instance Flag.instSetLikeFlag {α : Type u_1} [inst : LE α] :

SetLike (Flag α) α

Equations

Flag.instSetLikeFlag = { coe := Flag.carrier, coe_injective' := (_ : ∀ (s t : Flag α), s.carrier = t.carrier → s = t) }

source

ink

theorem Flag.ext {α : Type u_1} [inst : LE α] {s : Flag α} {t : Flag α} :

↑s = ↑t → s = t

source

ink

theorem Flag.mem_coe_iff {α : Type u_1} [inst : LE α] {s : Flag α} {a : α} :

a ∈ ↑s ↔ a ∈ s

source

ink

@[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) s → s ⊆ s → s = s) :

↑{ carrier := s, Chain' := h₁, max_chain' := h₂ } = s

source

ink

@[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) s → s.carrier ⊆ s → s.carrier = s) } = s

source

ink