mathlib3 documentation

order.chain

Chains and flags #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 α} :
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 y r' 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 s a b r 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 y s (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 = t s = 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_1 s s_1 s = 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