Documentation

Mathlib.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 IsChain {α : Type u_1} (r : ααProp) (s : Set α) :

A chain is a set s satisfying x ≺ y ∨ x = y ∨ y ≺ x for all x y ∈ s.

Equations
def SuperChain {α : Type u_1} (r : ααProp) (s : Set α) (t : Set α) :

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

Equations
def IsMaxChain {α : Type u_1} (r : ααProp) (s : Set α) :

A chain s is a maximal chain if there does not exists a chain strictly including s.

Equations
theorem isChain_empty {α : Type u_1} {r : ααProp} :
theorem Set.Subsingleton.isChain {α : Type u_1} {r : ααProp} {s : Set α} (hs : Set.Subsingleton s) :
theorem IsChain.mono {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
s tIsChain r tIsChain 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 yr' x y) :
IsChain r' s
theorem IsChain.symm {α : Type u_1} {r : ααProp} {s : Set α} (h : IsChain 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 α) :
theorem IsChain.insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : IsChain r s) (ha : bs, a br a b r b a) :
IsChain r (insert a s)
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 ys (f x) (f y)) {c : Set α} (hrc : IsChain r c) :
IsChain s (f '' c)
theorem Monotone.isChain_range {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : αβ} (hf : Monotone f) :
IsChain (fun (x x_1 : β) => x x_1) (Set.range f)
theorem IsChain.lt_of_le {α : Type u_1} [PartialOrder α] {s : Set α} (h : IsChain (fun (x x_1 : α) => x x_1) s) :
IsChain (fun (x x_1 : α) => x < x_1) 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) :
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 IsMaxChain.isChain {α : Type u_1} {r : ααProp} {s : Set α} (h : IsMaxChain r s) :
theorem IsMaxChain.not_superChain {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (h : IsMaxChain r s) :
theorem IsMaxChain.bot_mem {α : Type u_1} {s : Set α} [LE α] [OrderBot α] (h : IsMaxChain (fun (x x_1 : α) => x x_1) s) :
theorem IsMaxChain.top_mem {α : Type u_1} {s : Set α} [LE α] [OrderTop α] (h : IsMaxChain (fun (x x_1 : α) => x x_1) s) :
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
theorem succChain_spec {α : Type u_1} {r : ααProp} {s : Set α} (h : ∃ (t : Set α), IsChain r s SuperChain r s t) :
theorem IsChain.succ {α : Type u_1} {r : ααProp} {s : Set α} (hs : IsChain r s) :
theorem IsChain.superChain_succChain {α : Type u_1} {r : ααProp} {s : Set α} (hs₁ : IsChain r s) (hs₂ : ¬IsMaxChain r s) :
theorem subset_succChain {α : Type u_1} {r : ααProp} {s : Set α} :
inductive ChainClosure {α : Type u_1} (r : ααProp) :
Set αProp

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

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
theorem chainClosure_empty {α : Type u_1} {r : ααProp} :
theorem chainClosure_maxChain {α : Type u_1} {r : ααProp} :
theorem ChainClosure.total {α : Type u_1} {r : ααProp} {c₁ : Set α} {c₂ : Set α} (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) :
c₁ c₂ c₂ c₁
theorem ChainClosure.succ_fixpoint {α : Type u_1} {r : ααProp} {c₁ : Set α} {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) :
theorem ChainClosure.isChain {α : Type u_1} {r : ααProp} {c : Set α} (hc : ChainClosure r c) :
theorem maxChain_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) [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 (x x_1 : α) => x x_1) self.carrier

    By definition, a flag is a chain

  • max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun (x x_1 : α) => x x_1) sself.carrier sself.carrier = s

    By definition, a flag is a maximal chain

Instances For
instance Flag.instSetLikeFlag {α : Type u_1} [LE α] :
SetLike (Flag α) α
Equations
  • Flag.instSetLikeFlag = { coe := Flag.carrier, coe_injective' := }
theorem Flag.ext {α : Type u_1} [LE α] {s : Flag α} {t : Flag α} :
s = ts = 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 (x x_1 : α) => x x_1) s) (h₂ : ∀ ⦃s_1 : Set α⦄, IsChain (fun (x x_1 : α) => x x_1) s_1s s_1s = 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 (x x_1 : α) => x x_1) s
theorem Flag.maxChain {α : Type u_1} [LE α] (s : Flag α) :
IsMaxChain (fun (x x_1 : α) => x x_1) s
theorem Flag.top_mem {α : Type u_1} [LE α] [OrderTop α] (s : Flag α) :
theorem Flag.bot_mem {α : Type u_1} [LE α] [OrderBot α] (s : Flag α) :
theorem Flag.le_or_le {α : Type u_1} [Preorder α] {a : α} {b : α} (s : Flag α) (ha : a s) (hb : b s) :
a b b a
theorem Flag.chain_lt {α : Type u_1} [PartialOrder α] (s : Flag α) :
IsChain (fun (x x_1 : α) => x < x_1) s
instance Flag.instLinearOrderSubtypeMemFlagToLEToPreorderInstMembershipInstSetLikeFlag {α : Type u_1} [PartialOrder α] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : α) => x < x_1] (s : Flag α) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Flag.instUniqueFlagToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice = { toInhabited := { default := { carrier := Set.univ, Chain' := , max_chain' := } }, uniq := }