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

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

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)

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)

@[simp]

theorem IsChain.empty {α : Type u_1} {r : α → α → Prop} : IsChain r ∅

@[simp]

theorem IsChain.singleton {α : Type u_1} {r : α → α → Prop} {a : α} : IsChain r {a}

theorem Set.Subsingleton.isChain {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : s.Subsingleton) : IsChain r s

theorem IsChain.mono {α : Type u_1} {r : α → α → Prop} {s t : Set α} : s ⊆ t → IsChain r t → IsChain 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 y → r' x y) : IsChain r' s

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.

theorem isChain_of_trichotomous {α : Type u_1} {r : α → α → Prop} [Std.Trichotomous r] (s : Set α) : IsChain r s

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)

theorem IsChain.pair {α : Type u_1} {r : α → α → Prop} {a b : α} (h : r a b) : IsChain r {a, b}

theorem isChain_univ_iff {α : Type u_1} {r : α → α → Prop} : IsChain r Set.univ ↔ Std.Trichotomous r

theorem IsChain.image_of_map_rel {α : 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)

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)

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

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)

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)

theorem Antitone.isChain_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : Antitone f) (hs : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s) : IsChain (fun (x1 x2 : β) => x1 ≤ x2) (f '' s)

theorem Antitone.isChain_range {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} (hf : Antitone f) : IsChain (fun (x1 x2 : β) => x1 ≤ x2) (Set.range f)

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

@[simp]

theorem IsChain.diff {α : Type u_1} {r : α → α → Prop} {s t : Set α} (h : IsChain r s) : IsChain r (s \ t)

theorem isChain_preimage_subtypeVal {α : Type u_1} {r : α → α → Prop} (s t : Set α) : IsChain (fun (x1 x2 : ↑s) => r ↑x1 ↑x2) (Subtype.val ⁻¹' t) ↔ IsChain r (s ∩ t)

theorem isChain_coe_univ_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} : IsChain (fun (x1 x2 : ↑s) => r ↑x1 ↑x2) Set.univ ↔ IsChain r s

theorem IsChain.image {α : Type u_1} {β : Type u_2} {F : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} [FunLike F α β] [RelHomClass F r r'] (hs : IsChain r s) (φ : F) : IsChain r' (⇑φ '' s)

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)

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)

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

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

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)

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

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

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)

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

theorem IsChain.total {α : Type u_1} {r : α → α → Prop} {s : Set α} {x y : α} [Std.Refl 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 α} [Std.Refl r] (H : IsChain r s) : DirectedOn r s

theorem IsChain.directed {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Std.Refl 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 α} [Std.Refl 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

@[implicit_reducible]

def IsChain.linearOrder {α : Type u_1} [Preorder α] [DecidableLE α] {s : Set α} (hs : IsChain (fun (x1 x2 : α) => x1 < x2) s) : LinearOrder ↑s

A chain in a preorder is a linear order.

Equations

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

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

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

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

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

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 maximal_isChain_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} : Maximal (IsChain r) s ↔ IsMaxChain r s

theorem IsMaxChain.maximal_isChain {α : Type u_1} {r : α → α → Prop} {s : Set α} : IsMaxChain r s → Maximal (IsChain r) s

Alias of the reverse direction of maximal_isChain_iff.

theorem IsMaxChain.bot_mem {α : Type u_1} {s : Set α} [LE α] [OrderBot α] (h : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) s) : ⊥ ∈ s

theorem IsMaxChain.top_mem {α : Type u_1} {s : Set α} [LE α] [OrderTop α] (h : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) s) : ⊤ ∈ 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 IsMaxChain.isEmpty_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) : IsEmpty α ↔ s = ∅

theorem IsMaxChain.nonempty_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) : Nonempty α ↔ s.Nonempty

theorem IsMaxChain.symm {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) : IsMaxChain (flip r) s

noncomputable 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

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

theorem subset_succChain {α : Type u_1} {r : α → α → Prop} {s : Set α} : s ⊆ SuccChain r s

theorem List.IsChain.isChain_setOfPred_mem {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {l : List α} (h : IsChain r l) : _root_.IsChain r {a : α | a ∈ l}

Flags

structure Flag (α : Type u_4) [LE α] : Type u_4

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Flag.instPartialOrder {α : Type u_1} [LE α] : PartialOrder (Flag α)

Equations

• Flag.instPartialOrder = PartialOrder.ofSetLike (Flag α)

theorem Flag.ext {α : Type u_1} [LE α] {s t : Flag α} : ↑s = ↑t → s = t

theorem Flag.ext_iff {α : Type u_1} [LE α] {s t : Flag α} : s = t ↔ ↑s = ↑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 (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

@[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 (x1 x2 : α) => x1 ≤ x2) ↑s

theorem Flag.maxChain {α : Type u_1} [LE α] (s : Flag α) : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) ↑s

theorem Flag.top_mem {α : Type u_1} [LE α] [OrderTop α] (s : Flag α) : ⊤ ∈ s

theorem Flag.bot_mem {α : Type u_1} [LE α] [OrderBot α] (s : Flag α) : ⊥ ∈ 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

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

@[simp]

theorem Flag.coe_ofIsMaxChain {α : Type u_1} [LE α] (c : Set α) (hc : IsMaxChain (fun (x1 x2 : α) => x1 ≤ x2) c) : ↑(ofIsMaxChain c hc) = c

theorem Flag.le_or_le {α : Type u_1} [Preorder α] {a b : α} (s : Flag α) (ha : a ∈ s) (hb : b ∈ s) : a ≤ b ∨ b ≤ a

@[instance_reducible]

instance Flag.instOrderTopSubtypeMem {α : Type u_1} [Preorder α] [OrderTop α] (s : Flag α) : OrderTop ↥s

Equations

• s.instOrderTopSubtypeMem = Subtype.orderTop ⋯

@[instance_reducible]

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

Equations

• s.instOrderBotSubtypeMem = Subtype.orderBot ⋯

@[instance_reducible]

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

Equations

• s.instBoundedOrderSubtypeMem = Subtype.boundedOrder ⋯ ⋯

theorem Flag.mem_iff_forall_le_or_ge {α : Type u_1} [Preorder α] {a : α} {s : Flag α} : a ∈ s ↔ ∀ ⦃b : α⦄, b ∈ s → a ≤ b ∨ b ≤ a

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 := ⋯ }

@[simp]

theorem Flag.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) (s : Flag α) : ↑((map e) s) = ⇑e '' ↑s

@[simp]

theorem Flag.symm_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) : (map e).symm = map e.symm

theorem Flag.chain_lt {α : Type u_1} [PartialOrder α] (s : Flag α) : IsChain (fun (x1 x2 : α) => x1 < x2) ↑s

@[instance_reducible]

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.

@[instance_reducible]

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

Equations

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