mathlib documentation

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 #

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) :
theorem is_chain.mono {α : Type u_1} {r : α → α → Prop} {s t : set α} :
s tis_chain r tis_chain r s
theorem is_chain.mono_rel {α : Type u_1} {r : α → α → Prop} {s : set α} {r' : α → α → Prop} (h : is_chain r s) (h_imp : ∀ (x y : α), r x yr' x y) :
theorem is_chain.symm {α : Type u_1} {r : α → α → Prop} {s : set α} (h : is_chain r 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} [is_trichotomous α r] (s : set α) :
theorem is_chain.insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} (hs : is_chain r s) (ha : ∀ (b : α), b sa br a b r b a) :
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 : is_chain r c) :
is_chain s (f '' c)
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
theorem is_chain.directed_on {α : Type u_1} {r : α → α → Prop} {s : set α} [is_refl α r] (H : is_chain r s) :
@[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)
theorem is_chain.exists3 {α : Type u_1} {r : α → α → Prop} {s : set α} [is_refl α r] (hchain : is_chain r s) [is_trans α 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 : is_max_chain r s) :
theorem is_max_chain.not_super_chain {α : Type u_1} {r : α → α → Prop} {s t : set α} (h : is_max_chain r s) :
theorem is_max_chain.bot_mem {α : Type u_1} {s : set α} [has_le α] [order_bot α] (h : is_max_chain has_le.le s) :
theorem is_max_chain.top_mem {α : Type u_1} {s : set α} [has_le α] [order_top α] (h : is_max_chain has_le.le 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 α), is_chain r s super_chain r s t) :
theorem is_chain.succ {α : Type u_1} {r : α → α → Prop} {s : set α} (hs : is_chain r s) :
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) :
theorem subset_succ_chain {α : Type u_1} {r : α → α → Prop} {s : set α} :
inductive chain_closure {α : Type u_1} (r : α → α → Prop) :
set α → Prop

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₁ : chain_closure r c₁) (hc₂ : chain_closure r c₂) :
c₁ c₂ c₂ c₁
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₂
theorem chain_closure.succ_fixpoint_iff {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : chain_closure r c) :
theorem chain_closure.is_chain {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : chain_closure r 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₁ : is_chain has_le.le s) (h₂ : ∀ ⦃s_1 : set α⦄, is_chain has_le.le s_1s 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 α] [bounded_order α] (s : flag α) :
Equations
theorem flag.chain_lt {α : Type u_1} [partial_order α] (s : flag α) :
@[protected, instance]
Equations
@[protected, instance]
def flag.unique {α : Type u_1} [linear_order α] :
Equations