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 chains
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 #
super_chain s t
means that t
is a chain that strictly includes s
.
Equations
- super_chain r s t = (is_chain r t ∧ s ⊂ t)
theorem
set.subsingleton.is_chain
{α : Type u_1}
{r : α → α → Prop}
{s : set α}
(hs : s.subsingleton) :
is_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 y → r' x y) :
is_chain r' s
theorem
is_chain_of_trichotomous
{α : Type u_1}
{r : α → α → Prop}
[is_trichotomous α r]
(s : set α) :
is_chain r s
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 (has_insert.insert a s)
theorem
is_chain_univ_iff
{α : Type u_1}
{r : α → α → Prop} :
is_chain r set.univ ↔ is_trichotomous α r
theorem
is_chain.directed_on
{α : Type u_1}
{r : α → α → Prop}
{s : set α}
[is_refl α r]
(H : is_chain r s) :
directed_on r s
theorem
is_max_chain.is_chain
{α : Type u_1}
{r : α → α → Prop}
{s : set α}
(h : is_max_chain r s) :
is_chain r s
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
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) :
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
- succ_chain r s = dite (∃ (t : set α), is_chain r s ∧ super_chain r s t) (λ (h : ∃ (t : set α), is_chain r s ∧ super_chain r s t), classical.some h) (λ (h : ¬∃ (t : set α), is_chain r s ∧ super_chain r s t), s)
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)
theorem
is_chain.succ
{α : Type u_1}
{r : α → α → Prop}
{s : set α}
(hs : is_chain r s) :
is_chain r (succ_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) :
super_chain r s (succ_chain r s)
- succ : ∀ {α : Type u_1} {r : α → α → Prop} {s : set α}, chain_closure r s → chain_closure r (succ_chain r s)
- union : ∀ {α : Type u_1} {r : α → α → Prop} {s : set (set α)}, (∀ (a : set α), a ∈ s → chain_closure r a) → chain_closure r (⋃₀ s)
Predicate for whether a set is reachable from ∅
using succ_chain
and ⋃₀
.
An explicit maximal chain. max_chain
is taken to be the union of all sets in chain_closure
.
Equations
- max_chain r = ⋃₀ set_of (chain_closure r)
theorem
chain_closure.total
{α : Type u_1}
{r : α → α → Prop}
{c₁ c₂ : set α}
(hc₁ : chain_closure r c₁)
(hc₂ : chain_closure r 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) :
succ_chain r c = c ↔ c = max_chain r
theorem
chain_closure.is_chain
{α : Type u_1}
{r : α → α → Prop}
{c : set α}
(hc : chain_closure r c) :
is_chain r c
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 #
@[protected, instance]
Equations
- flag.set_like = {coe := flag.carrier _inst_1, coe_injective' := _}
@[simp]
@[protected]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def
flag.linear_order
{α : Type u_1}
[partial_order α]
[decidable_eq α]
[decidable_rel has_le.le]
[decidable_rel has_lt.lt]
(s : flag α) :
Equations
- s.linear_order = {le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ s)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ s)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := subtype.decidable_le (λ (x : α), x ∈ s), decidable_eq := subtype.decidable_eq (λ (a b : α), _inst_2 a b), decidable_lt := subtype.decidable_lt (λ (x : α), x ∈ s), max := max_default (λ (a b : ↥s), subtype.decidable_le a b), max_def := _, min := min_default (λ (a b : ↥s), subtype.decidable_le a b), min_def := _}
@[protected, instance]
Equations
- flag.unique = {to_inhabited := {default := {carrier := set.univ α, chain' := _, max_chain' := _}}, uniq := _}