doc-next-gen

Mathlib.Order.Preorder.Chain

Module docstring

{"# 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 ","### Flags "}

IsChain definition
(s : Set α) : Prop
Full source 
/-- A chain is a set `s` satisfying `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ s`. -/
def IsChain (s : Set α) : Prop :=
  s.Pairwise fun x y => x ≺ y ∨ y ≺ x
Chain in a partially ordered set
Informal description
A subset $s$ of a type $\alpha$ with a relation $\prec$ is called a *chain* if for any two distinct elements $x, y \in s$, either $x \prec y$ or $y \prec x$ holds.
SuperChain definition
(s t : Set α) : Prop
Full source 
/-- `SuperChain s t` means that `t` is a chain that strictly includes `s`. -/
def SuperChain (s t : Set α) : Prop :=
  IsChainIsChain r t ∧ s ⊂ t
Superchain of a set in a partially ordered set
Informal description
Given a relation `r` on a type `α`, a set `t` is a *superchain* of a set `s` if `t` is a chain (i.e., any two distinct elements in `t` are comparable under `r`) and `s` is a strict subset of `t`.
IsMaxChain definition
(s : Set α) : Prop
Full source 
/-- A chain `s` is a maximal chain if there does not exists a chain strictly including `s`. -/
def IsMaxChain (s : Set α) : Prop :=
  IsChainIsChain r s ∧ ∀ ⦃t⦄, IsChain r t → s ⊆ t → s = t
Maximal chain in a partially ordered set
Informal description
A subset $s$ of a type $\alpha$ with a relation $\prec$ is called a *maximal chain* if it is a chain (i.e., for any two distinct elements $x, y \in s$, either $x \prec y$ or $y \prec x$ holds) and there is no strictly larger chain containing $s$. In other words, for any chain $t$ containing $s$, we have $s = t$.
IsChain.empty theorem
: IsChain r ∅
Full source 
@[simp] lemma IsChain.empty : IsChain r ∅ := pairwise_empty _
Empty Set is a Chain
Informal description
The empty set is a chain for any relation $r$ on a type $\alpha$.
IsChain.singleton theorem
: IsChain r { a }
Full source 
@[simp] lemma IsChain.singleton : IsChain r {a} := pairwise_singleton ..
Singletons are Chains
Informal description
For any relation $r$ on a type $\alpha$ and any element $a \in \alpha$, the singleton set $\{a\}$ is a chain with respect to $r$.
Set.Subsingleton.isChain theorem
(hs : s.Subsingleton) : IsChain r s
Full source 
theorem Set.Subsingleton.isChain (hs : s.Subsingleton) : IsChain r s :=
  hs.pairwise _
Subsingleton Sets are Chains
Informal description
For any subset $s$ of a type $\alpha$ with a relation $\prec$, if $s$ is a subsingleton (i.e., contains at most one element), then $s$ is a chain with respect to $\prec$.
IsChain.mono theorem
: s ⊆ t → IsChain r t → IsChain r s
Full source 
theorem IsChain.mono : s ⊆ t → IsChain r t → IsChain r s :=
  Set.Pairwise.mono
Subset of a Chain is a Chain
Informal description
If a set $s$ is a subset of a set $t$ and $t$ is a chain with respect to a relation $r$, then $s$ is also a chain with respect to $r$.
IsChain.mono_rel theorem
{r' : α → α → Prop} (h : IsChain r s) (h_imp : ∀ x y, r x y → r' x y) : IsChain r' s
Full source 
theorem IsChain.mono_rel {r' : α → α → Prop} (h : IsChain r s) (h_imp : ∀ x y, r x y → r' x y) :
    IsChain r' s :=
  h.mono' fun x y => Or.imp (h_imp x y) (h_imp y x)
Chain Preservation Under Weaker Relation
Informal description
Let $r$ and $r'$ be two relations on a type $\alpha$, and let $s$ be a subset of $\alpha$. If $s$ is a chain with respect to $r$ (i.e., for any two distinct elements $x, y \in s$, either $r(x,y)$ or $r(y,x)$ holds), and if $r'$ is a relation such that $r(x,y)$ implies $r'(x,y)$ for all $x, y \in \alpha$, then $s$ is also a chain with respect to $r'$.
IsChain.symm theorem
(h : IsChain r s) : IsChain (flip r) s
Full source 
/-- This can be used to turn `IsChain (≥)` into `IsChain (≤)` and vice-versa. -/
theorem IsChain.symm (h : IsChain r s) : IsChain (flip r) s :=
  h.mono' fun _ _ => Or.symm
Chain Symmetry under Relation Flip
Informal description
For any relation $r$ on a type $\alpha$ and any subset $s$ of $\alpha$, if $s$ is a chain with respect to $r$, then $s$ is also a chain with respect to the flipped relation $\lambda x y, r y x$.
isChain_of_trichotomous theorem
[IsTrichotomous α r] (s : Set α) : IsChain r s
Full source 
theorem isChain_of_trichotomous [IsTrichotomous α r] (s : Set α) : IsChain r s :=
  fun a _ b _ hab => (trichotomous_of r a b).imp_right fun h => h.resolve_left hab
Trichotomous Relations Yield Chains
Informal description
For any set $s$ in a type $\alpha$ equipped with a trichotomous relation $r$ (i.e., for any $x, y \in \alpha$, exactly one of $x \prec y$, $y \prec x$, or $x = y$ holds), $s$ is a chain with respect to $r$.
IsChain.insert theorem
(hs : IsChain r s) (ha : ∀ b ∈ s, a ≠ b → a ≺ b ∨ b ≺ a) : IsChain r (insert a s)
Full source 
protected theorem IsChain.insert (hs : IsChain r s) (ha : ∀ b ∈ s, a ≠ b → a ≺ b ∨ b ≺ a) :
    IsChain r (insert a s) :=
  hs.insert_of_symmetric (fun _ _ => Or.symm) ha
Insertion Preserves Chain Property
Informal description
Let $s$ be a chain in a type $\alpha$ with respect to a relation $\prec$, and let $a$ be an element of $\alpha$. If for every $b \in s$ with $a \neq b$, either $a \prec b$ or $b \prec a$ holds, then the set obtained by inserting $a$ into $s$ is also a chain.
IsChain.pair theorem
(h : r a b) : IsChain r { a, b }
Full source 
lemma IsChain.pair (h : r a b) : IsChain r {a, b} :=
  IsChain.singleton.insert fun _ hb _ ↦ .inl <| (eq_of_mem_singleton hb).symm.recOn ‹_›
Pair of Related Elements Forms a Chain
Informal description
For any relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$ such that $a \prec b$, the pair $\{a, b\}$ forms a chain with respect to $r$.
isChain_univ_iff theorem
: IsChain r (univ : Set α) ↔ IsTrichotomous α r
Full source 
theorem isChain_univ_iff : IsChainIsChain r (univ : Set α) ↔ IsTrichotomous α r := by
  refine ⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
  rw [or_left_comm, or_iff_not_imp_left]
  exact h trivial trivial
Universal Set is a Chain iff Relation is Trichotomous
Informal description
The universal set (i.e., the entire type $\alpha$) is a chain with respect to a relation $r$ if and only if $r$ is trichotomous on $\alpha$, meaning that for any two elements $x, y \in \alpha$, exactly one of $x \prec y$, $y \prec x$, or $x = y$ holds.
IsChain.image theorem
(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)
Full source 
theorem IsChain.image (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) :=
  fun _ ⟨_, ha₁, ha₂⟩ _ ⟨_, hb₁, hb₂⟩ =>
  ha₂ ▸ hb₂ ▸ fun hxy => (hrc ha₁ hb₁ <| ne_of_apply_ne f hxy).imp (h _ _) (h _ _)
Image of a Chain under a Relation-Preserving Map is a Chain
Informal description
Let $r$ be a relation on $\alpha$, $s$ a relation on $\beta$, and $f : \alpha \to \beta$ a function such that for any $x, y \in \alpha$, if $r(x, y)$ holds then $s(f(x), f(y))$ holds. If $c \subseteq \alpha$ is a chain with respect to $r$, then the image $f(c)$ is a chain with respect to $s$.
isChain_union theorem
{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
Full source 
lemma isChain_union {s t : Set α} :
    IsChainIsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a := by
  rw [IsChain, IsChain, IsChain, pairwise_union_of_symmetric fun _ _ ↦ Or.symm]
Union of Two Sets is a Chain if and only if Each is a Chain and Elements are Related
Informal description
For any relation $r$ on a type $\alpha$ and any subsets $s, t \subseteq \alpha$, the union $s \cup t$ forms a chain with respect to $r$ if and only if: 1. $s$ is a chain with respect to $r$, 2. $t$ is a chain with respect to $r$, and 3. For any distinct elements $a \in s$ and $b \in t$, either $r(a, b)$ or $r(b, a)$ holds.
Monotone.isChain_image theorem
[Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : Monotone f) (hs : IsChain (· ≤ ·) s) : IsChain (· ≤ ·) (f '' s)
Full source 
lemma Monotone.isChain_image [Preorder α] [Preorder β] {s : Set α} {f : α → β}
    (hf : Monotone f) (hs : IsChain (· ≤ ·) s) : IsChain (· ≤ ·) (f '' s) :=
  hs.image _ _ _ (fun _ _ a ↦ hf a)
Image of a Chain under a Monotone Function is a Chain
Informal description
Let $\alpha$ and $\beta$ be preorders, $s$ a subset of $\alpha$, and $f : \alpha \to \beta$ a monotone function. If $s$ is a chain with respect to the non-strict order $\leq$ on $\alpha$, then the image $f(s)$ is a chain with respect to the non-strict order $\leq$ on $\beta$.
Monotone.isChain_range theorem
[LinearOrder α] [Preorder β] {f : α → β} (hf : Monotone f) : IsChain (· ≤ ·) (range f)
Full source 
theorem Monotone.isChain_range [LinearOrder α] [Preorder β] {f : α → β} (hf : Monotone f) :
    IsChain (· ≤ ·) (range f) := by
  rw [← image_univ]
  exact hf.isChain_image (isChain_of_trichotomous _)
Range of a Monotone Function from a Linear Order is a Chain
Informal description
Let $\alpha$ be a linearly ordered set and $\beta$ a preordered set. For any monotone function $f \colon \alpha \to \beta$, the range of $f$ is a chain with respect to the non-strict order $\leq$ on $\beta$.
IsChain.lt_of_le theorem
[PartialOrder α] {s : Set α} (h : IsChain (· ≤ ·) s) : IsChain (· < ·) s
Full source 
theorem IsChain.lt_of_le [PartialOrder α] {s : Set α} (h : IsChain (· ≤ ·) s) :
    IsChain (· < ·) s := fun _a ha _b hb hne ↦
  (h ha hb hne).imp hne.lt_of_le hne.lt_of_le'
Chain Preservation from Non-strict to Strict Order
Informal description
For any subset $s$ of a partially ordered set $\alpha$, if $s$ is a chain with respect to the relation $\leq$, then $s$ is also a chain with respect to the strict relation $<$.
IsChain.total theorem
(h : IsChain r s) (hx : x ∈ s) (hy : y ∈ s) : x ≺ y ∨ y ≺ x
Full source 
theorem IsChain.total (h : IsChain r s) (hx : x ∈ s) (hy : y ∈ s) : x ≺ y ∨ y ≺ x :=
  (eq_or_ne x y).elim (fun e => Or.inl <| e ▸ refl _) (h hx hy)
Total Comparability in a Chain
Informal description
For any chain $s$ with respect to a relation $\prec$ and any two elements $x, y \in s$, either $x \prec y$ or $y \prec x$ holds.
IsChain.directedOn theorem
(H : IsChain r s) : DirectedOn r s
Full source 
theorem IsChain.directedOn (H : IsChain r s) : DirectedOn r s := fun x hx y hy =>
  ((H.total hx hy).elim fun h => ⟨y, hy, h, refl _⟩) fun h => ⟨x, hx, refl _, h⟩
Directedness Property of Chains
Informal description
For any chain $s$ with respect to a relation $\prec$, the set $s$ is directed, meaning that for any two elements $x, y \in s$, there exists an element $z \in s$ such that $x \prec z$ and $y \prec z$.
IsChain.directed theorem
{f : β → α} {c : Set β} (h : IsChain (f ⁻¹'o r) c) : Directed r fun x : { a : β // a ∈ c } => f x
Full source 
protected theorem IsChain.directed {f : β → α} {c : Set β} (h : IsChain (f ⁻¹'o r) c) :
    Directed r fun x : { a : β // a ∈ c } => f x :=
  fun ⟨a, ha⟩ ⟨b, hb⟩ =>
    (by_cases fun hab : a = b => by
      simp only [hab, exists_prop, and_self_iff, Subtype.exists]
      exact ⟨b, hb, refl _⟩)
    fun hab => ((h ha hb hab).elim fun h => ⟨⟨b, hb⟩, h, refl _⟩) fun h => ⟨⟨a, ha⟩, refl _, h⟩
Directedness of a Function Restricted to a Chain
Informal description
Let $f : \beta \to \alpha$ be a function and $c \subseteq \beta$ be a subset such that the preimage of the relation $r$ under $f$ forms a chain on $c$. Then the restriction of $f$ to $c$ is directed with respect to $r$, meaning that for any two elements $x, y \in c$, there exists an element $z \in c$ such that $f(x) \prec_r f(z)$ and $f(y) \prec_r f(z)$.
IsChain.exists3 theorem
(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
Full source 
theorem IsChain.exists3 (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 := by
  rcases directedOn_iff_directed.mpr (IsChain.directed hchain) a mem1 b mem2 with ⟨z, mem4, H1, H2⟩
  rcases directedOn_iff_directed.mpr (IsChain.directed hchain) z mem4 c mem3 with
    ⟨z', mem5, H3, H4⟩
  exact ⟨z', mem5, _root_.trans H1 H3, _root_.trans H2 H3, H4⟩
Existence of Common Upper Bound for Three Elements in a Chain
Informal description
Let $s$ be a chain with respect to a transitive relation $r$ on a type $\alpha$, and let $a, b, c$ be three elements in $s$. Then there exists an element $z \in s$ such that $a \prec_r z$, $b \prec_r z$, and $c \prec_r z$.
IsChain.le_of_not_lt theorem
[Preorder α] (hs : IsChain (· ≤ ·) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬x < y) : y ≤ x
Full source 
lemma IsChain.le_of_not_lt [Preorder α] (hs : IsChain (· ≤ ·) s)
    {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬ x < y) : y ≤ x := by
  cases hs.total hx hy with
  | inr h' => exact h'
  | inl h' => simpa [lt_iff_le_not_le, h'] using h
Non-strict Order Property in Chains: $\neg(x < y) \Rightarrow y \leq x$
Informal description
Let $\alpha$ be a preorder and $s$ be a chain with respect to the relation $\leq$. For any two elements $x, y \in s$, if $x$ is not strictly less than $y$ (i.e., $\neg(x < y)$), then $y \leq x$.
IsChain.not_lt theorem
[Preorder α] (hs : IsChain (· ≤ ·) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : ¬x < y ↔ y ≤ x
Full source 
lemma IsChain.not_lt [Preorder α] (hs : IsChain (· ≤ ·) s)
    {x y : α} (hx : x ∈ s) (hy : y ∈ s) : ¬ x < y¬ x < y ↔ y ≤ x :=
  ⟨(hs.le_of_not_lt hx hy ·), fun h h' ↦ h'.not_le h⟩
Negation of Strict Order Relation in Chains: $\neg(x < y) \leftrightarrow y \leq x$
Informal description
Let $\alpha$ be a preorder and $s$ be a chain with respect to the relation $\leq$. For any two elements $x, y \in s$, the statement $\neg(x < y)$ is equivalent to $y \leq x$.
IsChain.lt_of_not_le theorem
[Preorder α] (hs : IsChain (· ≤ ·) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬x ≤ y) : y < x
Full source 
lemma IsChain.lt_of_not_le [Preorder α] (hs : IsChain (· ≤ ·) s)
    {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬ x ≤ y) : y < x :=
  (hs.total hx hy).elim (h · |>.elim) (lt_of_le_not_le · h)
Strict Order Property in Chains: $\neg(x \leq y) \Rightarrow y < x$
Informal description
Let $\alpha$ be a preorder and $s$ be a chain with respect to the relation $\leq$. For any two elements $x, y \in s$, if $x \nleq y$, then $y < x$.
IsChain.not_le theorem
[Preorder α] (hs : IsChain (· ≤ ·) s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : ¬x ≤ y ↔ y < x
Full source 
lemma IsChain.not_le [Preorder α] (hs : IsChain (· ≤ ·) s)
    {x y : α} (hx : x ∈ s) (hy : y ∈ s) : ¬ x ≤ y¬ x ≤ y ↔ y < x :=
  ⟨(hs.lt_of_not_le hx hy ·), fun h h' ↦ h'.not_lt h⟩
Negation of Order Relation in Chains: $\neg(x \leq y) \leftrightarrow y < x$
Informal description
Let $\alpha$ be a preorder and $s$ be a chain with respect to the relation $\leq$. For any two elements $x, y \in s$, the statement $\neg(x \leq y)$ is equivalent to $y < x$.
IsMaxChain.isChain theorem
(h : IsMaxChain r s) : IsChain r s
Full source 
theorem IsMaxChain.isChain (h : IsMaxChain r s) : IsChain r s :=
  h.1
Maximal chains are chains
Informal description
If $s$ is a maximal chain with respect to a relation $r$ on a type $\alpha$, then $s$ is also a chain with respect to $r$.
IsMaxChain.not_superChain theorem
(h : IsMaxChain r s) : ¬SuperChain r s t
Full source 
theorem IsMaxChain.not_superChain (h : IsMaxChain r s) : ¬SuperChain r s t := fun ht =>
  ht.2.ne <| h.2 ht.1 ht.2.1
Maximal chains have no proper superchains
Informal description
If $s$ is a maximal chain with respect to a relation $r$ on a type $\alpha$, then there does not exist any chain $t$ that strictly contains $s$ (i.e., $s$ is not a proper subset of any other chain $t$ with respect to $r$).
IsMaxChain.bot_mem theorem
[LE α] [OrderBot α] (h : IsMaxChain (· ≤ ·) s) : ⊥ ∈ s
Full source 
theorem IsMaxChain.bot_mem [LE α] [OrderBot α] (h : IsMaxChain (· ≤ ·) s) : ⊥⊥ ∈ s :=
  (h.2 (h.1.insert fun _ _ _ => Or.inl bot_le) <| subset_insert _ _).symm ▸ mem_insert _ _
Bottom Element Belongs to Every Maximal Chain in an Order with Bottom
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and a bottom element $\bot$. If $s$ is a maximal chain in $\alpha$ with respect to the order $\leq$, then the bottom element $\bot$ is contained in $s$.
IsMaxChain.top_mem theorem
[LE α] [OrderTop α] (h : IsMaxChain (· ≤ ·) s) : ⊤ ∈ s
Full source 
theorem IsMaxChain.top_mem [LE α] [OrderTop α] (h : IsMaxChain (· ≤ ·) s) : ⊤⊤ ∈ s :=
  (h.2 (h.1.insert fun _ _ _ => Or.inr le_top) <| subset_insert _ _).symm ▸ mem_insert _ _
Top Element Belongs to Every Maximal Chain in an Order with Top
Informal description
Let $\alpha$ be a type equipped with a partial order $\leq$ and a greatest element $\top$. If $s$ is a maximal chain in $\alpha$ with respect to the order $\leq$, then the top element $\top$ is contained in $s$.
IsMaxChain.image theorem
{s : β → β → Prop} (e : r ≃r s) {c : Set α} (hc : IsMaxChain r c) : IsMaxChain s (e '' c)
Full source 
lemma IsMaxChain.image {s : β → β → Prop} (e : r ≃r s) {c : Set α} (hc : IsMaxChain r c) :
    IsMaxChain s (e '' c) where
  left := hc.isChain.image _ _ _ fun _ _ ↦ by exact e.map_rel_iff.2
  right t ht hf := by
    rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, preimage_equiv_eq_image_symm]
    exact hc.2 (ht.image _ _ _ fun _ _ ↦ by exact e.symm.map_rel_iff.2)
      ((e.toEquiv.subset_symm_image _ _).2 hf)
Image of a Maximal Chain under Relation Isomorphism is Maximal Chain
Informal description
Let $r$ be a relation on $\alpha$ and $s$ a relation on $\beta$. Given a relation isomorphism $e : r \simeq s$ and a maximal chain $c \subseteq \alpha$ with respect to $r$, the image $e(c) \subseteq \beta$ is a maximal chain with respect to $s$.
SuccChain definition
(r : α → α → Prop) (s : Set α) : Set α
Full source 
/-- 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`. -/
def SuccChain (r : α → α → Prop) (s : Set α) : Set α :=
  if h : ∃ t, IsChain r s ∧ SuperChain r s t then h.choose else s
Successor chain of a set with respect to a relation
Informal description
Given a relation $r$ on a type $\alpha$ and a subset $s \subseteq \alpha$, the *successor chain* of $s$, denoted $\text{SuccChain}(r, s)$, is defined as follows: if there exists a chain $t$ (with respect to $r$) that strictly contains $s$, then $\text{SuccChain}(r, s)$ is one such chain; otherwise, it is $s$ itself.
succChain_spec theorem
(h : ∃ t, IsChain r s ∧ SuperChain r s t) : SuperChain r s (SuccChain r s)
Full source 
theorem succChain_spec (h : ∃ t, IsChain r s ∧ SuperChain r s t) :
    SuperChain r s (SuccChain r s) := by
  have : IsChainIsChain r s ∧ SuperChain r s h.choose := h.choose_spec
  simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2
Successor Chain Specification: Existence of Superchain Implies Successor Chain is Superchain
Informal description
Given a relation $r$ on a type $\alpha$ and a subset $s \subseteq \alpha$, if there exists a chain $t$ (with respect to $r$) such that $s$ is a chain and $t$ is a superchain of $s$, then the successor chain $\text{SuccChain}(r, s)$ is a superchain of $s$.
IsChain.succ theorem
(hs : IsChain r s) : IsChain r (SuccChain r s)
Full source 
theorem IsChain.succ (hs : IsChain r s) : IsChain r (SuccChain r s) :=
  if h : ∃ t, IsChain r s ∧ SuperChain r s t then (succChain_spec h).1
  else by
    rw [exists_and_left] at h
    simpa [SuccChain, dif_neg, h] using hs
Successor Chain Preserves Chain Property
Informal description
For any relation $r$ on a type $\alpha$ and any subset $s \subseteq \alpha$, if $s$ is a chain with respect to $r$, then its successor chain $\text{SuccChain}(r, s)$ is also a chain with respect to $r$.
IsChain.superChain_succChain theorem
(hs₁ : IsChain r s) (hs₂ : ¬IsMaxChain r s) : SuperChain r s (SuccChain r s)
Full source 
theorem IsChain.superChain_succChain (hs₁ : IsChain r s) (hs₂ : ¬IsMaxChain r s) :
    SuperChain r s (SuccChain r s) := by
  simp only [IsMaxChain, _root_.not_and, not_forall, exists_prop, exists_and_left] at hs₂
  obtain ⟨t, ht, hst⟩ := hs₂ hs₁
  exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩
Existence of Superchain for Non-Maximal Chains
Informal description
Let $r$ be a relation on a type $\alpha$ and $s \subseteq \alpha$ be a chain with respect to $r$. If $s$ is not a maximal chain, then its successor chain $\text{SuccChain}(r, s)$ is a superchain of $s$ (i.e., $s$ is strictly contained in $\text{SuccChain}(r, s)$ and $\text{SuccChain}(r, s)$ is also a chain with respect to $r$).
Flag structure
(α : Type*) [LE α]
Full source 
/-- The type of flags, aka maximal chains, of an order. -/
structure Flag (α : Type*) [LE α] where
  /-- The `carrier` of a flag is the underlying set. -/
  carrier : Set α
  /-- By definition, a flag is a chain -/
  Chain' : IsChain (· ≤ ·) carrier
  /-- By definition, a flag is a maximal chain -/
  max_chain' : ∀ ⦃s⦄, IsChain (· ≤ ·) s → carrier ⊆ s → carrier = s
Flag (maximal chain) in a partially ordered set
Informal description
A flag (or maximal chain) in a partially ordered set $(α, \leq)$ is a subset of $α$ that is totally ordered under $\leq$ and is maximal with respect to inclusion among all such totally ordered subsets.
Flag.instSetLike instance
: SetLike (Flag α) α
Full source 
instance : SetLike (Flag α) α where
  coe := carrier
  coe_injective' s t h := by
    cases s
    cases t
    congr
Flags as Set-like Structures
Informal description
The type of flags (maximal chains) in a partially ordered set $\alpha$ can be treated as a set-like structure, meaning that flags can be viewed as subsets of $\alpha$ with the usual membership relation.
Flag.ext theorem
: (s : Set α) = t → s = t
Full source 
@[ext]
theorem ext : (s : Set α) = t → s = t :=
  SetLike.ext'
Extensionality of Flags: $s = t$ implies $s$ and $t$ are equal as flags
Informal description
For any two sets $s$ and $t$ in a partially ordered set $\alpha$, if $s$ and $t$ are equal as sets, then they are equal as flags (maximal chains).
Flag.mem_coe_iff theorem
: a ∈ (s : Set α) ↔ a ∈ s
Full source 
theorem mem_coe_iff : a ∈ (s : Set α)a ∈ (s : Set α) ↔ a ∈ s :=
  Iff.rfl
Membership in Flag as Set vs. Membership in Flag
Informal description
For any element $a$ and any flag $s$ in a partially ordered set $\alpha$, the element $a$ belongs to the underlying set of $s$ if and only if $a$ belongs to $s$ as a flag.
Flag.coe_mk theorem
(s : Set α) (h₁ h₂) : (mk s h₁ h₂ : Set α) = s
Full source 
@[simp]
theorem coe_mk (s : Set α) (h₁ h₂) : (mk s h₁ h₂ : Set α) = s :=
  rfl
Flag Construction Preserves Underlying Set
Informal description
For any subset $s$ of a partially ordered set $\alpha$, and for any proofs $h_1$ that $s$ is a chain and $h_2$ that $s$ is maximal, the underlying set of the flag constructed from $s$, $h_1$, and $h_2$ is equal to $s$ itself.
Flag.mk_coe theorem
(s : Flag α) : mk (s : Set α) s.Chain' s.max_chain' = s
Full source 
@[simp]
theorem mk_coe (s : Flag α) : mk (s : Set α) s.Chain' s.max_chain' = s :=
  ext rfl
Flag Reconstruction Identity: $\text{mk}(s) = s$
Informal description
For any flag $s$ in a partially ordered set $\alpha$, constructing a new flag from the underlying set of $s$ and its chain and maximality properties yields $s$ itself. That is, $\text{mk}(s, \text{Chain'}(s), \text{max\_chain'}(s)) = s$.
Flag.chain_le theorem
(s : Flag α) : IsChain (· ≤ ·) (s : Set α)
Full source 
theorem chain_le (s : Flag α) : IsChain (· ≤ ·) (s : Set α) :=
  s.Chain'
Flags are chains with respect to the order relation
Informal description
For any flag (maximal chain) $s$ in a partially ordered set $\alpha$, the underlying set of $s$ is a chain with respect to the order relation $\leq$.
Flag.maxChain theorem
(s : Flag α) : IsMaxChain (· ≤ ·) (s : Set α)
Full source 
protected theorem maxChain (s : Flag α) : IsMaxChain (· ≤ ·) (s : Set α) :=
  ⟨s.chain_le, s.max_chain'⟩
Flags are maximal chains in a partially ordered set
Informal description
For any flag $s$ in a partially ordered set $\alpha$, the underlying set of $s$ is a maximal chain with respect to the order relation $\leq$.
Flag.top_mem theorem
[OrderTop α] (s : Flag α) : (⊤ : α) ∈ s
Full source 
theorem top_mem [OrderTop α] (s : Flag α) : (⊤ : α) ∈ s :=
  s.maxChain.top_mem
Top Element Belongs to Every Flag in an Order with Top
Informal description
Let $\alpha$ be a partially ordered set with a greatest element $\top$. For any flag (maximal chain) $s$ in $\alpha$, the top element $\top$ belongs to $s$.
Flag.bot_mem theorem
[OrderBot α] (s : Flag α) : (⊥ : α) ∈ s
Full source 
theorem bot_mem [OrderBot α] (s : Flag α) : (⊥ : α) ∈ s :=
  s.maxChain.bot_mem
Bottom Element Belongs to Every Flag in an Order with Bottom
Informal description
Let $\alpha$ be a partially ordered set with a bottom element $\bot$. For any flag (maximal chain) $s$ in $\alpha$, the bottom element $\bot$ is contained in $s$.
Flag.ofIsMaxChain definition
(c : Set α) (hc : IsMaxChain (· ≤ ·) c) : Flag α
Full source 
/-- Reinterpret a maximal chain as a flag. -/
def ofIsMaxChain (c : Set α) (hc : IsMaxChain (· ≤ ·) c) : Flag α := ⟨c, hc.isChain, hc.2⟩
Flag from maximal chain
Informal description
Given a subset $c$ of a partially ordered set $\alpha$ that is a maximal chain with respect to the order relation $\leq$, the function constructs a flag (maximal chain) from $c$.
Flag.coe_ofIsMaxChain theorem
(c : Set α) (hc) : ofIsMaxChain c hc = c
Full source 
@[simp, norm_cast]
lemma coe_ofIsMaxChain (c : Set α) (hc) : ofIsMaxChain c hc = c := rfl
Flag Construction Preserves Underlying Set
Informal description
For any subset $c$ of a partially ordered set $\alpha$ that is a maximal chain with respect to the order relation $\leq$, the underlying set of the flag constructed from $c$ via `ofIsMaxChain` is equal to $c$ itself. In other words, $\text{ofIsMaxChain}(c, hc) = c$.
Flag.le_or_le theorem
(s : Flag α) (ha : a ∈ s) (hb : b ∈ s) : a ≤ b ∨ b ≤ a
Full source 
protected theorem le_or_le (s : Flag α) (ha : a ∈ s) (hb : b ∈ s) : a ≤ b ∨ b ≤ a :=
  s.chain_le.total ha hb
Total Comparability in Flags
Informal description
For any flag (maximal chain) $s$ in a partially ordered set $\alpha$ and any two elements $a, b \in s$, either $a \leq b$ or $b \leq a$ holds.
Flag.instOrderTopSubtypeMem instance
[OrderTop α] (s : Flag α) : OrderTop s
Full source 
instance [OrderTop α] (s : Flag α) : OrderTop s :=
  Subtype.orderTop s.top_mem
Inheritance of Top Element in Flags
Informal description
For any partially ordered set $\alpha$ with a greatest element $\top$ and any flag (maximal chain) $s$ in $\alpha$, the subtype corresponding to $s$ inherits the order structure with $\top$ as its greatest element.
Flag.instOrderBotSubtypeMem instance
[OrderBot α] (s : Flag α) : OrderBot s
Full source 
instance [OrderBot α] (s : Flag α) : OrderBot s :=
  Subtype.orderBot s.bot_mem
Inheritance of Bottom Element in Flags
Informal description
For any partially ordered set $\alpha$ with a least element $\bot$ and any flag (maximal chain) $s$ in $\alpha$, the subtype corresponding to $s$ inherits the order structure with $\bot$ as its least element.
Flag.instBoundedOrderSubtypeMem instance
[BoundedOrder α] (s : Flag α) : BoundedOrder s
Full source 
instance [BoundedOrder α] (s : Flag α) : BoundedOrder s :=
  Subtype.boundedOrder s.bot_mem s.top_mem
Inheritance of Bounded Order Structure in Flags
Informal description
For any bounded order $\alpha$ and any flag (maximal chain) $s$ in $\alpha$, the subtype corresponding to $s$ inherits a bounded order structure from $\alpha$.
Flag.mem_iff_forall_le_or_ge theorem
: a ∈ s ↔ ∀ ⦃b⦄, b ∈ s → a ≤ b ∨ b ≤ a
Full source 
lemma mem_iff_forall_le_or_ge : a ∈ sa ∈ s ↔ ∀ ⦃b⦄, b ∈ s → a ≤ b ∨ b ≤ a :=
  ⟨fun ha b => s.le_or_le ha, fun hb =>
    of_not_not fun ha =>
      Set.ne_insert_of_not_mem _ ‹_› <|
        s.maxChain.2 (s.chain_le.insert fun c hc _ => hb hc) <| Set.subset_insert _ _⟩
Membership Criterion for Flags via Total Comparability
Informal description
An element $a$ belongs to a flag (maximal chain) $s$ in a partially ordered set $\alpha$ if and only if for every element $b \in s$, either $a \leq b$ or $b \leq a$ holds.
Flag.map definition
(e : α ≃o β) : Flag α ≃ Flag β
Full source 
/-- Flags are preserved under order isomorphisms. -/
def map (e : α ≃o β) : FlagFlag α ≃ Flag β where
  toFun s := ofIsMaxChain _ (s.maxChain.image e)
  invFun s := ofIsMaxChain _ (s.maxChain.image e.symm)
  left_inv s := ext <| e.symm_image_image s
  right_inv s := ext <| e.image_symm_image s
Bijection between flags induced by an order isomorphism
Informal description
Given an order isomorphism $e : \alpha \simeq_o \beta$ between partially ordered sets $\alpha$ and $\beta$, the function maps a flag (maximal chain) $s$ in $\alpha$ to the flag obtained by applying $e$ to all elements of $s$. This mapping is bijective, with its inverse being the mapping induced by the inverse order isomorphism $e^{-1} : \beta \simeq_o \alpha$. More precisely: 1. For any flag $s$ in $\alpha$, the image $e''s$ (the set $\{e(x) | x \in s\}$) forms a flag in $\beta$ 2. The mapping $s \mapsto e''s$ is bijective between flags of $\alpha$ and flags of $\beta$ 3. The inverse mapping is given by $t \mapsto e^{-1}''t$ for flags $t$ in $\beta$
Flag.coe_map theorem
(e : α ≃o β) (s : Flag α) : ↑(map e s) = e '' s
Full source 
@[simp, norm_cast] lemma coe_map (e : α ≃o β) (s : Flag α) : ↑(map e s) = e '' s := rfl
Image of Flag under Order Isomorphism Equals Direct Image
Informal description
For any order isomorphism $e : \alpha \simeq_o \beta$ between partially ordered sets $\alpha$ and $\beta$, and any flag (maximal chain) $s$ in $\alpha$, the underlying set of the image flag $\text{map}(e)(s)$ is equal to the image of $s$ under $e$, i.e., $\text{map}(e)(s) = e''s$.
Flag.symm_map theorem
(e : α ≃o β) : (map e).symm = map e.symm
Full source 
@[simp] lemma symm_map (e : α ≃o β) : (map e).symm = map e.symm := rfl
Inverse of Flag Mapping Induced by Order Isomorphism
Informal description
Given an order isomorphism $e : \alpha \simeq_o \beta$ between partially ordered sets $\alpha$ and $\beta$, the inverse of the induced flag mapping $e'' : \text{Flag}(\alpha) \simeq \text{Flag}(\beta)$ is equal to the flag mapping induced by the inverse order isomorphism $e^{-1} : \beta \simeq_o \alpha$.
Flag.chain_lt theorem
(s : Flag α) : IsChain (· < ·) (s : Set α)
Full source 
theorem chain_lt (s : Flag α) : IsChain (· < ·) (s : Set α) := s.chain_le.lt_of_le
Flags are chains with respect to the strict order relation
Informal description
For any flag (maximal chain) $s$ in a partially ordered set $\alpha$, the underlying set of $s$ is a chain with respect to the strict order relation $<$.
Flag.instLinearOrderSubtypeMemOfDecidableLEOfDecidableLTOfDecidableEq instance
[DecidableLE α] [DecidableLT α] [DecidableEq α] (s : Flag α) : LinearOrder s
Full source 
instance [DecidableLE α] [DecidableLT α] [DecidableEq α] (s : Flag α) : LinearOrder s :=
  { Subtype.partialOrder _ with
    le_total := fun a b => s.le_or_le a.2 b.2
    toDecidableLE := Subtype.decidableLE
    toDecidableLT := Subtype.decidableLT
    toDecidableEq := Subtype.instDecidableEq }
Linear Order Structure on Flags in Partially Ordered Sets
Informal description
For any flag (maximal chain) $s$ in a partially ordered set $\alpha$ with decidable $\leq$, $<$, and $=$, the subset $s$ inherits a linear order structure from $\alpha$.