Set.chainHeight_dual
theorem Set.chainHeight_dual :
∀ {α : Type u_1} [inst : LT α] (s : Set α), (⇑OrderDual.ofDual ⁻¹' s).chainHeight = s.chainHeight
This theorem states that for any set `s` of a type `α` under a less-than relation (`LT α`), the maximal length of a strictly ascending sequence (also known as the chain height) remains the same whether we consider the set `s` or its order dual. The order dual of a set is the set with the reverse order. So, this theorem basically says that reversing the order of a set does not change the maximal length of strictly ascending sequences within the set.
More concisely: For any set `s` of type `α` under a less-than relation `LT α`, the maximal length of a strictly ascending sequence in `s` equals the maximal length of a strictly ascending sequence in its order dual.
|
Set.le_chainHeight_iff
theorem Set.le_chainHeight_iff :
∀ {α : Type u_1} [inst : LT α] {s : Set α} {n : ℕ}, ↑n ≤ s.chainHeight ↔ ∃ l ∈ s.subchain, l.length = n
The theorem `Set.le_chainHeight_iff` states that for any type `α` that has a less than relation (`LT α`), any set `s` of type `α`, and any natural number `n`, `n` is less than or equal to the chain height of set `s` if and only if there exists a list `l` in the subchains of set `s` such that the length of list `l` is `n`. In essence, this theorem relates the chain height of a set, which is the maximum length of a strictly ascending sequence in the set, with the existence of a strictly ascending list of specific length within the set.
More concisely: The chain height of a set equals the length of a strict ascending sequence in it if and only if there exists such a sequence of length equal to a given natural number.
|