# Chains and flags #

This file defines chains for an arbitrary relation and flags for an order.

## Main declarations #

- `IsChain s`: A chain `s` 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 #

source
def IsChain {α : 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

- IsChain r s = s.Pairwise fun (x y : α) => r x y ∨ r y x

Instances For

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

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

Equations

- SuperChain r s t = (IsChain r t ∧ s ⊂ t)

Instances For

source
def IsMaxChain {α : 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

- IsMaxChain r s = (IsChain r s ∧ ∀ ⦃t : Set α⦄, IsChain r t → s ⊆ t → s = t)

Instances For

source
@[simp]
theorem IsChain.empty {α : Type u_1} {r : α → α → Prop} :
IsChain r ∅
source
@[simp]
theorem IsChain.singleton {α : Type u_1} {r : α → α → Prop} {a : α} :
IsChain r {a}
source
theorem Set.Subsingleton.isChain {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : s.Subsingleton) :
IsChain r s
source
theorem IsChain.mono {α : Type u_1} {r : α → α → Prop} {s t : Set α} :
s ⊆ t → IsChain r t → IsChain r s
source
theorem IsChain.mono_rel {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop} (h : IsChain r s) (h_imp : ∀ (x y : α), r x y → r' x y) :
IsChain r' s
source
theorem IsChain.symm {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsChain r s) :
IsChain (flip r) s

This can be used to turn `IsChain (≥)` into `IsChain (≤)` and vice-versa.

source
theorem isChain_of_trichotomous {α : Type u_1} {r : α → α → Prop} [IsTrichotomous α r] (s : Set α) :
IsChain r s
source
theorem IsChain.insert {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (hs : IsChain r s) (ha : ∀ b ∈ s, a ≠ b → r a b ∨ r b a) :
IsChain r (insert a s)
source
theorem IsChain.pair {α : Type u_1} {r : α → α → Prop} {a b : α} (h : r a b) :
IsChain r {a, b}
source
theorem isChain_univ_iff {α : Type u_1} {r : α → α → Prop} :
IsChain r Set.univ ↔ IsTrichotomous α r
source
theorem IsChain.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 : IsChain r c) :
IsChain s (f '' c)
source
theorem IsChain.preimage {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (f : α → β) (hf : Function.Injective f) (h : ∀ (x y : α), s (f x) (f y) → r x y) {c : Set β} (hrc : IsChain s c) :
IsChain r (f ⁻¹' c)
source
theorem isChain_union {α : Type u_1} {r : α → α → Prop} {s t : Set α} :
IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
source
theorem Monotone.isChain_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : Monotone f) (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) :
IsChain (fun (x1 x2 : β) => x1 ≤ x2) (f '' s)
source
theorem Monotone.isChain_range {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} (hf : Monotone f) :
IsChain (fun (x1 x2 : β) => x1 ≤ x2) (Set.range f)
source
theorem IsChain.lt_of_le {α : Type u_1} [PartialOrder α] {s : Set α} (h : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) :
IsChain (fun (x1 x2 : α) => x1 < x2) s
source
theorem IsChain.image_relEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} (hs : IsChain r s) (φ : r ↪r r') :
IsChain r' (⇑φ '' s)
source
theorem IsChain.preimage_relEmbedding {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β} (ht : IsChain r' t) (φ : r ↪r r') :
IsChain r (⇑φ ⁻¹' t)
source
theorem IsChain.image_relIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} (hs : IsChain r s) (φ : r ≃r r') :
IsChain r' (⇑φ '' s)
source
theorem IsChain.preimage_relIso {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β} (hs : IsChain r' t) (φ : r ≃r r') :
IsChain r (⇑φ ⁻¹' t)
source
theorem IsChain.image_relEmbedding_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ↪r r'} :
IsChain r' (⇑φ '' s) ↔ IsChain r s
source
theorem IsChain.image_relIso_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ≃r r'} :
IsChain r' (⇑φ '' s) ↔ IsChain r s
source
theorem IsChain.image_embedding {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) (φ : α ↪o β) :
IsChain (fun (x1 x2 : β) => x1 ≤ x2) (⇑φ '' s)
source
theorem IsChain.preimage_embedding {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} (ht : IsChain (fun (x1 x2 : β) => x1 ≤ x2) t) (φ : α ↪o β) :
IsChain (fun (x1 x2 : α) => x1 ≤ x2) (⇑φ ⁻¹' t)
source
theorem IsChain.image_embedding_iff {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] {φ : α ↪o β} :
IsChain (fun (x1 x2 : β) => x1 ≤ x2) (⇑φ '' s) ↔ IsChain (fun (x1 x2 : α) => x1 ≤ x2) s
source
theorem IsChain.image_iso {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) (φ : α ≃o β) :
IsChain (fun (x1 x2 : β) => x1 ≤ x2) (⇑φ '' s)
source
theorem IsChain.image_iso_iff {α : Type u_1} {β : Type u_2} {s : Set α} [LE α] [LE β] {φ : α ≃o β} :
IsChain (fun (x1 x2 : β) => x1 ≤ x2) (⇑φ '' s) ↔ IsChain (fun (x1 x2 : α) => x1 ≤ x2) s
source
theorem IsChain.preimage_iso {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} (ht : IsChain (fun (x1 x2 : β) => x1 ≤ x2) t) (φ : α ≃o β) :
IsChain (fun (x1 x2 : α) => x1 ≤ x2) (⇑φ ⁻¹' t)
source
theorem IsChain.preimage_iso_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {t : Set β} {φ : α ≃o β} :
IsChain (fun (x1 x2 : α) => x1 ≤ x2) (⇑φ ⁻¹' t) ↔ IsChain (fun (x1 x2 : β) => x1 ≤ x2) t
source
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
source
theorem IsChain.directedOn {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsRefl α r] (H : IsChain r s) :
DirectedOn r s
source
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
source
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
source
theorem IsChain.le_of_not_gt {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬x < y) :
y ≤ x
source
@[deprecated IsChain.le_of_not_gt (since := "2025-05-11")]
theorem IsChain.le_of_not_lt {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬x < y) :
y ≤ x

Alias of `IsChain.le_of_not_gt`.

source
theorem IsChain.not_lt {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) :
¬x < y ↔ y ≤ x
source
theorem IsChain.lt_of_not_ge {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬x ≤ y) :
y < x
source
@[deprecated IsChain.lt_of_not_ge (since := "2025-05-11")]
theorem IsChain.lt_of_not_le {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬x ≤ y) :
y < x

Alias of `IsChain.lt_of_not_ge`.

source
theorem IsChain.not_le {α : Type u_1} {s : Set α} [Preorder α] (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) :
¬x ≤ y ↔ y < x
source
theorem IsMaxChain.isChain {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) :
IsChain r s
source
theorem IsMaxChain.not_superChain {α : Type u_1} {r : α → α → Prop} {s t : Set α} (h : IsMaxChain r s) :
¬SuperChain r s t
source
theorem IsMaxChain.bot_mem {α : Type u_1} {s : Set α} [LE α] [OrderBot α] (h : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) s) :
⊥ ∈ s
source
theorem IsMaxChain.top_mem {α : Type u_1} {s : Set α} [LE α] [OrderTop α] (h : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) s) :
⊤ ∈ s
source
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)
source
theorem IsMaxChain.isEmpty_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) :
IsEmpty α ↔ s = ∅
source
theorem IsMaxChain.nonempty_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) :
Nonempty α ↔ s ≠ ∅
source
theorem IsMaxChain.symm {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) :
IsMaxChain (flip r) s
source
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

- SuccChain r s = if h : ∃ (t : Set α), IsChain r s ∧ SuperChain r s t then h.choose else s

Instances For

source
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)
source
theorem IsChain.succ {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsChain r s) :
IsChain r (SuccChain r s)
source
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)
source
theorem subset_succChain {α : Type u_1} {r : α → α → Prop} {s : Set α} :
s ⊆ SuccChain r s

### Flags #

source
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 (x1 x2 : α) => x1 ≤ x2) self.carrier

  By definition, a flag is a chain

- max_chain' ⦃s : Set α⦄ : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s → self.carrier ⊆ s → self.carrier = s

  By definition, a flag is a maximal chain

Instances For

source
instance Flag.instSetLike {α : Type u_1} [LE α] :
SetLike (Flag α) α
Equations

- Flag.instSetLike = { coe := Flag.carrier, coe_injective' := ⋯ }

source
theorem Flag.ext {α : Type u_1} [LE α] {s t : Flag α} :
↑s = ↑t → s = t
source
theorem Flag.ext_iff {α : Type u_1} [LE α] {s t : Flag α} :
s = t ↔ ↑s = ↑t
source
theorem Flag.mem_coe_iff {α : Type u_1} [LE α] {s : Flag α} {a : α} :
a ∈ ↑s ↔ a ∈ s
source
@[simp]
theorem Flag.coe_mk {α : Type u_1} [LE α] (s : Set α) (h₁ : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) (h₂ : ∀ ⦃s_1 : Set α⦄, IsChain (fun (x1 x2 : α) => x1 ≤ x2) s_1 → s ⊆ s_1 → s = s_1) :
↑{ carrier := s, Chain' := h₁, max_chain' := h₂ } = s
source
@[simp]
theorem Flag.mk_coe {α : Type u_1} [LE α] (s : Flag α) :
{ carrier := ↑s, Chain' := ⋯, max_chain' := ⋯ } = s
source
theorem Flag.chain_le {α : Type u_1} [LE α] (s : Flag α) :
IsChain (fun (x1 x2 : α) => x1 ≤ x2) ↑s
source
theorem Flag.maxChain {α : Type u_1} [LE α] (s : Flag α) :
IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) ↑s
source
theorem Flag.top_mem {α : Type u_1} [LE α] [OrderTop α] (s : Flag α) :
⊤ ∈ s
source
theorem Flag.bot_mem {α : Type u_1} [LE α] [OrderBot α] (s : Flag α) :
⊥ ∈ s
source
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

- Flag.ofIsMaxChain c hc = { carrier := c, Chain' := ⋯, max_chain' := ⋯ }

Instances For

source
@[simp]
theorem Flag.coe_ofIsMaxChain {α : Type u_1} [LE α] (c : Set α) (hc : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) c) :
↑(ofIsMaxChain c hc) = c
source
theorem Flag.le_or_le {α : Type u_1} [Preorder α] {a b : α} (s : Flag α) (ha : a ∈ s) (hb : b ∈ s) :
a ≤ b ∨ b ≤ a
source
instance Flag.instOrderTopSubtypeMem {α : Type u_1} [Preorder α] [OrderTop α] (s : Flag α) :
OrderTop ↥s
Equations

- s.instOrderTopSubtypeMem = Subtype.orderTop ⋯

source
instance Flag.instOrderBotSubtypeMem {α : Type u_1} [Preorder α] [OrderBot α] (s : Flag α) :
OrderBot ↥s
Equations

- s.instOrderBotSubtypeMem = Subtype.orderBot ⋯

source
instance Flag.instBoundedOrderSubtypeMem {α : Type u_1} [Preorder α] [BoundedOrder α] (s : Flag α) :
BoundedOrder ↥s
Equations

- s.instBoundedOrderSubtypeMem = Subtype.boundedOrder ⋯ ⋯

source
theorem Flag.mem_iff_forall_le_or_ge {α : Type u_1} [Preorder α] {a : α} {s : Flag α} :
a ∈ s ↔ ∀ ⦃b : α⦄, b ∈ s → a ≤ b ∨ b ≤ a
source
def Flag.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) :
Flag α ≃ Flag β

Flags are preserved under order isomorphisms.

Equations

- Flag.map e = { toFun := fun (s : Flag α) => Flag.ofIsMaxChain (⇑e '' ↑s) ⋯, invFun := fun (s : Flag β) => Flag.ofIsMaxChain (⇑e.symm '' ↑s) ⋯, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Flag.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) (s : Flag α) :
↑((map e) s) = ⇑e '' ↑s
source
@[simp]
theorem Flag.symm_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) :
(map e).symm = map e.symm
source
theorem Flag.chain_lt {α : Type u_1} [PartialOrder α] (s : Flag α) :
IsChain (fun (x1 x2 : α) => x1 < x2) ↑s
source
instance Flag.instLinearOrderSubtypeMemOfDecidableLEOfDecidableLTOfDecidableEq {α : Type u_1} [PartialOrder α] [DecidableLE α] [DecidableLT α] [DecidableEq α] (s : Flag α) :
LinearOrder ↥s
Equations

- One or more equations did not get rendered due to their size.

source
instance Flag.instUnique {α : Type u_1} [LinearOrder α] :
Unique (Flag α)
Equations

- Flag.instUnique = { default := { carrier := Set.univ, Chain' := ⋯, max_chain' := ⋯ }, uniq := ⋯ }