Chains and flags #
This file defines chains for an arbitrary relation and flags for an order.
Main declarations #
IsChain s
: A chains
is a set of comparable elements.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 #
@[deprecated IsChain.empty (since := "2024-11-25")]
Alias of IsChain.empty
.
theorem
Set.Subsingleton.isChain
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(hs : s.Subsingleton)
:
IsChain r s
theorem
isChain_of_trichotomous
{α : Type u_1}
{r : α → α → Prop}
[IsTrichotomous α r]
(s : Set α)
:
IsChain r s
theorem
Monotone.isChain_range
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
{f : α → β}
(hf : Monotone f)
:
theorem
IsChain.lt_of_le
{α : Type u_1}
[PartialOrder α]
{s : Set α}
(h : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
IsChain.directedOn
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
[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 t : Set α}
(h : IsMaxChain r s)
:
¬SuperChain r s t
theorem
IsMaxChain.bot_mem
{α : Type u_1}
{s : Set α}
[LE α]
[OrderBot α]
(h : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
IsMaxChain.top_mem
{α : Type u_1}
{s : Set α}
[LE α]
[OrderTop α]
(h : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
IsMaxChain.image
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{s : β → β → Prop}
(e : r ≃r s)
{c : Set α}
(hc : IsMaxChain r c)
:
IsMaxChain s (⇑e '' c)
theorem
succChain_spec
{α : Type u_1}
{r : α → α → Prop}
{s : Set α}
(h : ∃ (t : Set α), 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)
Flags #
theorem
Flag.maxChain
{α : Type u_1}
[LE α]
(s : Flag α)
:
IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) ↑s
def
Flag.ofIsMaxChain
{α : Type u_1}
[LE α]
(c : Set α)
(hc : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) c)
:
Flag α
Reinterpret a maximal chain as a flag.
Equations
Instances For
@[simp]
theorem
Flag.coe_ofIsMaxChain
{α : Type u_1}
[LE α]
(c : Set α)
(hc : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) c)
:
instance
Flag.instBoundedOrderSubtypeMem
{α : Type u_1}
[Preorder α]
[BoundedOrder α]
(s : Flag α)
:
BoundedOrder ↥s
Equations
instance
Flag.instLinearOrderSubtypeMemOfDecidableLEOfDecidableLTOfDecidableEq
{α : Type u_1}
[PartialOrder α]
[DecidableLE α]
[DecidableLT α]
[DecidableEq α]
(s : Flag α)
:
LinearOrder ↥s