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 #

• is_chain s: A chain s is a set of comparable elements.
• max_chain_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 is_chain {α : 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
def super_chain {α : Type u_1} (r : α → α → Prop) (s t : set α) :
Prop

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

Equations
def is_max_chain {α : 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
theorem is_chain_empty {α : Type u_1} {r : α → α → Prop} :
theorem set.subsingleton.is_chain {α : Type u_1} {r : α → α → Prop} {s : set α} (hs : s.subsingleton) :
s
theorem is_chain.mono {α : Type u_1} {r : α → α → Prop} {s t : set α} :
s t t s
theorem is_chain.mono_rel {α : Type u_1} {r : α → α → Prop} {s : set α} {r' : α → α → Prop} (h : s) (h_imp : ∀ (x y : α), r x yr' x y) :
theorem is_chain.symm {α : Type u_1} {r : α → α → Prop} {s : set α} (h : s) :

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

theorem is_chain_of_trichotomous {α : Type u_1} {r : α → α → Prop} [ r] (s : set α) :
s
theorem is_chain.insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} (hs : s) (ha : ∀ (b : α), b sa br a b r b a) :
s)
theorem is_chain_univ_iff {α : Type u_1} {r : α → α → Prop} :
theorem is_chain.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 : c) :
(f '' c)
theorem is_chain.total {α : Type u_1} {r : α → α → Prop} {s : set α} {x y : α} [ r] (h : s) (hx : x s) (hy : y s) :
r x y r y x
theorem is_chain.directed_on {α : Type u_1} {r : α → α → Prop} {s : set α} [ r] (H : s) :
s
@[protected]
theorem is_chain.directed {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [ r] {f : β → α} {c : set β} (h : is_chain (f ⁻¹'o r) c) :
(λ (x : {a // a c}), f x)
theorem is_chain.exists3 {α : Type u_1} {r : α → α → Prop} {s : set α} [ r] (hchain : s) [ r] {a b c : α} (mem1 : a s) (mem2 : b s) (mem3 : c s) :
∃ (z : α) (mem4 : z s), r a z r b z r c z
theorem is_max_chain.is_chain {α : Type u_1} {r : α → α → Prop} {s : set α} (h : s) :
s
theorem is_max_chain.not_super_chain {α : Type u_1} {r : α → α → Prop} {s t : set α} (h : s) :
¬ s t
theorem is_max_chain.bot_mem {α : Type u_1} {s : set α} [has_le α] [order_bot α] (h : s) :
theorem is_max_chain.top_mem {α : Type u_1} {s : set α} [has_le α] [order_top α] (h : s) :
def succ_chain {α : Type u_1} (r : α → α → Prop) (s : set α) :
set α

Given a set s, if there exists a chain t strictly including s, then succ_chain s is one of these chains. Otherwise it is s.

Equations
theorem succ_chain_spec {α : Type u_1} {r : α → α → Prop} {s : set α} (h : ∃ (t : set α), s s t) :
s s)
theorem is_chain.succ {α : Type u_1} {r : α → α → Prop} {s : set α} (hs : s) :
s)
theorem is_chain.super_chain_succ_chain {α : Type u_1} {r : α → α → Prop} {s : set α} (hs₁ : s) (hs₂ : ¬ s) :
s s)
theorem subset_succ_chain {α : Type u_1} {r : α → α → Prop} {s : set α} :
s s
inductive chain_closure {α : Type u_1} (r : α → α → Prop) :
set α → Prop
• succ : ∀ {α : Type u_1} {r : α → α → Prop} {s : set α}, s)
• union : ∀ {α : Type u_1} {r : α → α → Prop} {s : set (set α)}, (∀ (a : set α), a s a) (⋃₀ s)

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

def max_chain {α : Type u_1} (r : α → α → Prop) :
set α

An explicit maximal chain. max_chain is taken to be the union of all sets in chain_closure.

Equations
theorem chain_closure_empty {α : Type u_1} {r : α → α → Prop} :
theorem chain_closure_max_chain {α : Type u_1} {r : α → α → Prop} :
theorem chain_closure.total {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : c₁) (hc₂ : c₂) :
c₁ c₂ c₂ c₁
theorem chain_closure.succ_fixpoint {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : c₁) (hc₂ : c₂) (hc : c₂ = c₂) :
c₁ c₂
theorem chain_closure.succ_fixpoint_iff {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : c) :
c = c c =
theorem chain_closure.is_chain {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : c) :
c
theorem max_chain_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) [has_le α] :
Type u_3

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

Instances for flag
@[protected, instance]
def flag.set_like {α : Type u_1} [has_le α] :
set_like (flag α) α
Equations
@[ext]
theorem flag.ext {α : Type u_1} [has_le α] {s t : flag α} :
s = ts = t
@[simp]
theorem flag.mem_coe_iff {α : Type u_1} [has_le α] {s : flag α} {a : α} :
a s a s
@[simp]
theorem flag.coe_mk {α : Type u_1} [has_le α] (s : set α) (h₁ : s) (h₂ : ∀ ⦃s_1 : set α⦄, s s_1s = s_1) :
{carrier := s, chain' := h₁, max_chain' := h₂} = s
@[simp]
theorem flag.mk_coe {α : Type u_1} [has_le α] (s : flag α) :
{carrier := s, chain' := _, max_chain' := _} = s
theorem flag.chain_le {α : Type u_1} [has_le α] (s : flag α) :
@[protected]
theorem flag.max_chain {α : Type u_1} [has_le α] (s : flag α) :
theorem flag.top_mem {α : Type u_1} [has_le α] [order_top α] (s : flag α) :
theorem flag.bot_mem {α : Type u_1} [has_le α] [order_bot α] (s : flag α) :
@[protected]
theorem flag.le_or_le {α : Type u_1} [preorder α] {a b : α} (s : flag α) (ha : a s) (hb : b s) :
a b b a
@[protected, instance]
def flag.order_top {α : Type u_1} [preorder α] [order_top α] (s : flag α) :
Equations
@[protected, instance]
def flag.order_bot {α : Type u_1} [preorder α] [order_bot α] (s : flag α) :
Equations
@[protected, instance]
def flag.bounded_order {α : Type u_1} [preorder α] (s : flag α) :
Equations
theorem flag.chain_lt {α : Type u_1} (s : flag α) :
@[protected, instance]
def flag.linear_order {α : Type u_1} [decidable_eq α] (s : flag α) :
Equations
@[protected, instance]
def flag.unique {α : Type u_1} [linear_order α] :
Equations