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 α) : Prop

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

def SuperChain {α : Type u_1} (r : α → α → Prop) (s 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)

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)

@[simp]

theorem IsChain.empty {α : Type u_1} {r : α → α → Prop} : IsChain r ∅

@[simp]

theorem IsChain.singleton {α : Type u_1} {r : α → α → Prop} {a : α} : IsChain r {a}

@[deprecated IsChain.empty (since := "2024-11-25")]

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

Alias of IsChain.empty.

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

theorem IsChain.mono {α : Type u_1} {r : α → α → Prop} {s t : Set α} : s ⊆ t → IsChain r t → IsChain 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 y → r' x y) : IsChain r' s

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.

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

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

theorem IsChain.pair {α : Type u_1} {r : α → α → Prop} {a b : α} (h : r a b) : IsChain r {a, b}

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 y → s (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 ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r 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) : DirectedOn 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) : IsChain r s

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

theorem IsMaxChain.bot_mem {α : Type u_1} {s : Set α} [LE α] [OrderBot α] (h : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) s) : ⊥ ∈ s

theorem IsMaxChain.top_mem {α : Type u_1} {s : Set α} [LE α] [OrderTop α] (h : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) s) : ⊤ ∈ 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

• SuccChain r s = if h : ∃ (t : Set α), IsChain r s ∧ SuperChain r s t then h.choose else s

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

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

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)

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

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

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

• 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 ∈ s, ChainClosure r a) → ChainClosure r (⋃₀ s)

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)

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

theorem chainClosure_maxChain {α : Type u_1} {r : α → α → Prop} : ChainClosure r (maxChain r)

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

theorem ChainClosure.succ_fixpoint {α : Type u_1} {r : α → α → Prop} {c₁ 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) : SuccChain r c = c ↔ c = maxChain r

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

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

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) s → self.carrier ⊆ s → self.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 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_1 → s ⊆ s_1 → s = 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 α) : ⊤ ∈ s

theorem Flag.bot_mem {α : Type u_1} [LE α] [OrderBot α] (s : Flag α) : ⊥ ∈ s

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

• Flag.ofIsMaxChain c hc = { carrier := c, Chain' := ⋯, max_chain' := ⋯ }

@[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 α) : OrderTop ↥s

Equations

• s.instOrderTopSubtypeMem = Subtype.orderTop ⋯

instance Flag.instOrderBotSubtypeMem {α : Type u_1} [Preorder α] [OrderBot α] (s : Flag α) : OrderBot ↥s

Equations

• s.instOrderBotSubtypeMem = Subtype.orderBot ⋯

instance Flag.instBoundedOrderSubtypeMem {α : Type u_1} [Preorder α] [BoundedOrder α] (s : Flag α) : BoundedOrder ↥s

Equations

• s.instBoundedOrderSubtypeMem = Subtype.boundedOrder ⋯ ⋯

theorem Flag.mem_iff_forall_le_or_ge {α : Type u_1} [Preorder α] {a : α} {s : Flag α} : a ∈ s ↔ ∀ ⦃b : α⦄, b ∈ s → a ≤ 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

• Flag.map e = { toFun := fun (s : Flag α) => Flag.ofIsMaxChain (⇑e '' ↑s) ⋯, invFun := fun (s : Flag β) => Flag.ofIsMaxChain (⇑e.symm '' ↑s) ⋯, left_inv := ⋯, right_inv := ⋯ }

@[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.instLinearOrderSubtypeMemOfLeOfDecidableRelLt {α : Type u_1} [PartialOrder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : α) => x1 < x2] (s : Flag α) : LinearOrder ↥s

Equations

• s.instLinearOrderSubtypeMemOfLeOfDecidableRelLt = LinearOrder.mk ⋯ Subtype.decidableLE decidableEqOfDecidableLE Subtype.decidableLT ⋯ ⋯ ⋯

instance Flag.instUnique {α : Type u_1} [LinearOrder α] : Unique (Flag α)

Equations

• Flag.instUnique = { default := { carrier := Set.univ, Chain' := ⋯, max_chain' := ⋯ }, uniq := ⋯ }