mathlib documentation

order.chain

Chains #

This file defines chains for an arbitrary relation 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.

source
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
source
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
source
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
source
theorem is_chain_empty {α : Type u_1} {r : α → α → Prop} :
is_chain r ∅
source
theorem set.subsingleton.is_chain {α : Type u_1} {r : α → α → Prop} {s : set α} (hs : s.subsingleton) :
is_chain r s
source
theorem is_chain.mono {α : Type u_1} {r : α → α → Prop} {s t : set α} :
s ⊆ t → is_chain r t → is_chain r s
source
theorem is_chain.symm {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_chain r s) :
is_chain (flip r) s

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

source
theorem is_chain_of_trichotomous {α : Type u_1} {r : α → α → Prop} [is_trichotomous α r] (s : set α) :
is_chain r s
source
theorem is_chain.insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} (hs : is_chain r s) (ha : ∀ (b : α), b ∈ s → a ≠ b → r a b ∨ r b a) :
is_chain r (insert a s)
source
theorem is_chain_univ_iff {α : Type u_1} {r : α → α → Prop} :
is_chain r set.univ ↔ is_trichotomous α r
source
theorem is_chain.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 : is_chain r c) :
is_chain s (f '' c)
source
theorem is_chain.total {α : Type u_1} {r : α → α → Prop} {s : set α} {x y : α} [is_refl α r] (h : is_chain r s) (hx : x ∈ s) (hy : y ∈ s) :
r x y ∨ r y x
source
theorem is_chain.directed_on {α : Type u_1} {r : α → α → Prop} {s : set α} [is_refl α r] (H : is_chain r s) :
directed_on r s
source
@[protected]
theorem is_chain.directed {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [is_refl α r] {f : β → α} {c : set β} (h : is_chain (f ⁻¹'o r) c) :
directed r (λ (x : {a // a ∈ c}), f ↑x)
source
theorem is_max_chain.is_chain {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_max_chain r s) :
is_chain r s
source
theorem is_max_chain.not_super_chain {α : Type u_1} {r : α → α → Prop} {s t : set α} (h : is_max_chain r s) :
¬super_chain r s t
source
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
source
theorem succ_chain_spec {α : Type u_1} {r : α → α → Prop} {s : set α} (h : ∃ (t : set α), is_chain r s ∧ super_chain r s t) :
super_chain r s (succ_chain r s)
source
theorem is_chain.succ {α : Type u_1} {r : α → α → Prop} {s : set α} (hs : is_chain r s) :
is_chain r (succ_chain r s)
source
theorem is_chain.super_chain_succ_chain {α : Type u_1} {r : α → α → Prop} {s : set α} (hs₁ : is_chain r s) (hs₂ : ¬is_max_chain r s) :
super_chain r s (succ_chain r s)
source
theorem subset_succ_chain {α : Type u_1} {r : α → α → Prop} {s : set α} :
s ⊆ succ_chain r s
source
inductive chain_closure {α : Type u_1} (r : α → α → Prop) :
set α → Prop

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

source
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
source
theorem chain_closure_empty {α : Type u_1} {r : α → α → Prop} :
chain_closure r ∅
source
theorem chain_closure_max_chain {α : Type u_1} {r : α → α → Prop} :
chain_closure r (max_chain r)
source
theorem chain_closure.total {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂) :
c₁ ⊆ c₂ ∨ c₂ ⊆ c₁
source
theorem chain_closure.succ_fixpoint {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂) (hc : succ_chain r c₂ = c₂) :
c₁ ⊆ c₂
source
theorem chain_closure.succ_fixpoint_iff {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : chain_closure r c) :
succ_chain r c = c ↔ c = max_chain r
source
theorem chain_closure.is_chain {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : chain_closure r c) :
is_chain r c
source
theorem max_chain_spec {α : Type u_1} {r : α → α → Prop} :
is_max_chain r (max_chain 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.