Flag.maxChain
theorem Flag.maxChain : ∀ {α : Type u_1} [inst : LE α] (s : Flag α), IsMaxChain (fun x x_1 => x ≤ x_1) ↑s
The theorem `Flag.maxChain` states that for any type `α` that has a less than or equal to (`≤`) relation and for any flag `s` of this type, `s` is a maximal chain with respect to the `≤` relation. In other words, `s` is a chain where there is no other chain that strictly includes `s`. If there is a chain `t` that includes `s`, then `t` must be equal to `s`. Here, a chain is a set of elements where any two distinct elements are comparable (one is less than or equal to the other).
More concisely: For any type `α` with a total order `≤` and any flag `s` of `α`, `s` is a maximal chain with respect to `≤`, meaning there is no strictly larger chain containing `s`.
|
IsChain.symm
theorem IsChain.symm : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsChain r s → IsChain (flip r) s
This theorem states that for any type `α`, a relation `r`, and a set `s`, if `s` is a chain with respect to the relation `r`, then `s` is also a chain with respect to the flipped relation of `r`. In other words, if all elements in the set `s` are related pairwise by either `r x y` or `r y x` (making `s` a chain), then all elements in `s` are also related pairwise by either `flip r y x` or `flip r x y`. This is particularly useful for reversing the direction of an ordered relation, such as turning a chain in non-ascending order (`IsChain (≥)`) into a chain in non-descending order (`IsChain (≤)`) and vice-versa.
More concisely: given a type `α` and a binary relation `r` on `α`, if `s` is a chain with respect to `r`, then `s` is also a chain with respect to the flipped relation `flip r`.
|
IsChain.total
theorem IsChain.total :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {x y : α} [inst : IsRefl α r],
IsChain r s → x ∈ s → y ∈ s → r x y ∨ r y x
This theorem states that for any type `α` and any binary relation `r` on `α`, if a set `s` of type `α` is a chain (i.e., for all elements `x` and `y` in `s`, `r x y`, `r y x`, or `x = y` holds), then for all elements `x` and `y` in `s`, `r x y` or `r y x` holds. Furthermore, the relation `r` is reflexive, meaning for all `x` in `α`, `r x x` holds. This theorem is very significant in the study of order relations, particularly in proving the properties of chains in partially ordered sets.
More concisely: In a reflexive binary relation on a type, any chain is a total order.
|
Flag.max_chain'
theorem Flag.max_chain' :
∀ {α : Type u_3} [inst : LE α] (self : Flag α) ⦃s : Set α⦄,
IsChain (fun x x_1 => x ≤ x_1) s → self.carrier ⊆ s → self.carrier = s
This theorem states that, given a type `α` with a less-than-or-equal-to (`≤`) relation and a `Flag` on `α`, for any set `s` of `α` which forms a chain with respect to the `≤` relation, if the `Flag` is a subset of `s`, then the `Flag` must be equal to `s`. In other words, a `Flag` is defined as a maximal chain, meaning that it includes all elements from any other chain it is a subset of.
More concisely: If `α` is a type with a `≤` relation and `Flag(α)` is a maximal chain in `α` with respect to `≤`, then `Flag(α)` equals the set of all elements in any chain contained in `Flag(α)` that is a subset of `Flag(α)`.
|
IsChain.directedOn
theorem IsChain.directedOn :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [inst : IsRefl α r], IsChain r s → DirectedOn r s
This theorem states that for any type `α`, any relation `r` on `α`, and any set `s` of `α`, if `r` is a reflexive relation (meaning for all `x` in `α`, `r x x` holds) and `s` is a chain with respect to `r` (meaning for all `x` and `y` in `s`, either `x` is related to `y`, `y` is related to `x`, or `x` and `y` are the same), then `s` is also directed with respect to `r`. A set is directed with respect to a relation if, for any two elements in the set, there exists a third element in the set that is related to both of them.
More concisely: If `r` is a reflexive relation on type `α` and `s` is a chain of `α` with respect to `r`, then `s` is a directed set with respect to `r`.
|
isChain_of_trichotomous
theorem isChain_of_trichotomous :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsTrichotomous α r] (s : Set α), IsChain r s
This theorem, named `isChain_of_trichotomous`, states that for any type `α` and a relation `r` on `α`, if the relation `r` is trichotomous, meaning for any two elements `x` and `y` in `α`, either `r x y`, `x = y`, or `r y x` holds, then any set `s` of elements from `α` is a chain with respect to the relation `r`. In other words, it states that if a relation is trichotomous, then all elements of a set are pairwise comparable under that relation, highlighting the property of a chain.
More concisely: For any type `α` and trichotomous relation `r` on `α`, any set `s` of elements from `α` forms a chain with respect to `r`.
|
IsChain.insert
theorem IsChain.insert :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
IsChain r s → (∀ b ∈ s, a ≠ b → r a b ∨ r b a) → IsChain r (insert a s)
The theorem `IsChain.insert` states that for any type `α`, any binary relation `r` on `α`, any set `s` of elements of type `α`, and any element `a` of type `α`, if `s` forms a chain with respect to `r` and for every element `b` in `s` such that `a` is not equal to `b`, either `r a b` or `r b a` holds, then the set obtained by inserting `a` into `s` also forms a chain with respect to `r`. In other words, inserting a new element into a chain, which relates to every element in the chain, preserves the chain property.
More concisely: If `s` is a chain with respect to `r` and `a` is not in `s`, then `s ∪ {a}` is a chain with respect to `r` if and only if for all `b` in `s`, either `r(a, b)` or `r(b, a)` holds.
|
maxChain_spec
theorem maxChain_spec : ∀ {α : Type u_1} {r : α → α → Prop}, IsMaxChain r (maxChain r)
**Hausdorff's Maximality Principle**
The theorem states that for any type `α` and any binary relation `r` on `α`, there exists a maximal chain according to `r`. Here, a maximal chain is defined as a set for which there does not exist any other chain that strictly contains it. The chain is determined by the `maxChain` function, which is the union of all sets in the `ChainClosure` of `r`. Notably, the relation `r` does not need to impose a partial order on `α` for this maximality principle to hold.
More concisely: For any type `α` and binary relation `r` on `α`, there exists a maximal chain, which is the union of all sets in the transitive closure of `r`, according to `r`. (This statement is equivalent to the one given, but may be more concise for mathematical purposes.)
|
Flag.Chain'
theorem Flag.Chain' : ∀ {α : Type u_3} [inst : LE α] (self : Flag α), IsChain (fun x x_1 => x ≤ x_1) self.carrier := by
sorry
The theorem `Flag.Chain'` states that for any type `α` with a less than or equal to (`≤`) relation, and for any instance of a `Flag` over `α`, the underlying carrier set of the `Flag` is a chain. In other words, for any two elements `x` and `x_1` in the `Flag`, either `x` is less than or equal to `x_1` or `x_1` is less than or equal to `x`, satisfying the definition of a chain.
More concisely: For any type equipped with a reflexive and transitive `≤` relation, and for any `Flag` over it, the flags underlying carrier set forms a chain.
|
Flag.chain_le
theorem Flag.chain_le : ∀ {α : Type u_1} [inst : LE α] (s : Flag α), IsChain (fun x x_1 => x ≤ x_1) ↑s
The theorem `Flag.chain_le` states that for any type `α` equipped with a less than or equal to relation, and for any set `s` of type `Flag α`, `s` is a chain with respect to the less than or equal to relation. In other words, for all pairs of elements `x` and `y` in `s`, either `x` is less than or equal to `y`, or `y` is less than or equal to `x`. Thus, `s` satisfies the property defined by `IsChain`.
More concisely: For any set `s` of type `Flag α` in a type `α` equipped with a total order, `s` is a chain with respect to the order relation.
|
succChain_spec
theorem succChain_spec :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
(∃ t, IsChain r s ∧ SuperChain r s t) → SuperChain r s (SuccChain r s)
The theorem `succChain_spec` states that for any type `α`, relation `r`, and set `s` of type `α`, if there exists a chain `t` which is both a chain in the relation `r` and a superchain of `s`, then the successor chain of `s` (as computed by `SuccChain`) is also a superchain of `s` in the relation `r`. This implies that the `SuccChain` function correctly finds a superchain whenever one exists.
More concisely: If a relation `r` on type `α` has a chain `t` that is both a chain in `r` and a superchain of a set `s`, then the successor chain of `s` in `r` (as computed by `SuccChain`) is also a superchain of `s`.
|