Chains and flags #
This file defines chains for an arbitrary relation and flags for an order and proves Hausdorff's Maximality Principle.
Main declarations #
IsChain s
: A chains
is a set of comparable elements.maxChain_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 #
theorem
Set.Subsingleton.isChain
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(hs : Set.Subsingleton s)
:
IsChain r s
theorem
isChain_of_trichotomous
{α : Type u_1}
{r : α → α → Prop}
[inst : IsTrichotomous α r]
(s : Set α)
:
IsChain r s
theorem
IsChain.directedOn
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
[inst : IsRefl α r]
(H : IsChain r s)
:
DirectedOn r s
theorem
IsMaxChain.isChain
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(h : IsMaxChain r s)
:
IsChain r s
theorem
IsMaxChain.not_superChain
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
{t : Set α}
(h : IsMaxChain r s)
:
¬SuperChain r s t
theorem
succChain_spec
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(h : ∃ t, IsChain r s ∧ SuperChain r s t)
:
SuperChain r s (SuccChain r s)
theorem
IsChain.superChain_succChain
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(hs₁ : IsChain r s)
(hs₂ : ¬IsMaxChain r s)
:
SuperChain r s (SuccChain r s)
- succ: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, ChainClosure r s → ChainClosure r (SuccChain r s)
- union: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set (Set α)}, (∀ (a : Set α), a ∈ s → ChainClosure r a) → ChainClosure r (⋃₀ s)
Predicate for whether a set is reachable from ∅∅
using SuccChain
and ⋃₀⋃₀
.
Instances For
theorem
ChainClosure.total
{α : Type u_1}
{r : α → α → Prop}
{c₁ : Set α}
{c₂ : Set α}
(hc₁ : ChainClosure r c₁)
(hc₂ : ChainClosure r 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.isChain
{α : Type u_1}
{r : α → α → Prop}
{c : Set α}
(hc : ChainClosure r c)
:
IsChain 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 #
theorem
Flag.maxChain
{α : Type u_1}
[inst : LE α]
(s : Flag α)
:
IsMaxChain (fun x x_1 => x ≤ x_1) ↑s
instance
Flag.instOrderTopSubtypeMemFlagToLEInstMembershipInstSetLikeFlagLe
{α : Type u_1}
[inst : Preorder α]
[inst : OrderTop α]
(s : Flag α)
:
Equations
instance
Flag.instOrderBotSubtypeMemFlagToLEInstMembershipInstSetLikeFlagLe
{α : Type u_1}
[inst : Preorder α]
[inst : OrderBot α]
(s : Flag α)
:
Equations
instance
Flag.instBoundedOrderSubtypeMemFlagToLEInstMembershipInstSetLikeFlagLe
{α : Type u_1}
[inst : Preorder α]
[inst : BoundedOrder α]
(s : Flag α)
:
BoundedOrder { x // x ∈ s }
Equations
- Flag.instBoundedOrderSubtypeMemFlagToLEInstMembershipInstSetLikeFlagLe s = Subtype.boundedOrder (_ : ⊥ ∈ s) (_ : ⊤ ∈ s)
instance
Flag.instLinearOrderSubtypeMemFlagToLEToPreorderInstMembershipInstSetLikeFlag
{α : Type u_1}
[inst : PartialOrder α]
[inst : DecidableRel fun x x_1 => x ≤ x_1]
[inst : DecidableRel fun x x_1 => x < x_1]
(s : Flag α)
:
LinearOrder { x // x ∈ s }
Equations
- One or more equations did not get rendered due to their size.
instance
Flag.instUniqueFlagToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice
{α : Type u_1}
[inst : LinearOrder α]
:
Equations
- One or more equations did not get rendered due to their size.