RelEmbedding.acc_iff_no_decreasing_seq
theorem RelEmbedding.acc_iff_no_decreasing_seq :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsStrictOrder α r] {x : α},
Acc r x ↔ IsEmpty { f // x ∈ Set.range ⇑f }
This theorem states that for any type `α` and a relation `r` on `α` which is a strict order, a value `x` of type `α` is accessible if and only if there isn't any decreasing sequence that contains `x`. Here, a decreasing sequence is defined as a sequence where every successive element is smaller than the previous one according to the relation `r`. The sequence is represented as a function `f` for which `x` is in its range. The `IsEmpty` construct indicates the non-existence of such a sequence.
More concisely: For any type `α` and strict order relation `r` on `α`, an element `x` is accessible if and only if there does not exist a decreasing sequence `f` with domain containing `x` according to `r`.
|
exists_increasing_or_nonincreasing_subseq
theorem exists_increasing_or_nonincreasing_subseq :
∀ {α : Type u_1} (r : α → α → Prop) [inst : IsTrans α r] (f : ℕ → α),
∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
This Lean theorem, named `exists_increasing_or_nonincreasing_subseq`, states the infinitary Erdős–Szekeres theorem and is a crucial lemma in the conventional proof of the Bolzano-Weierstrass theorem for real numbers. Specifically, for any type `α`, a binary relation `r` on `α` that is transitive, and a sequence `f` of elements of type `α` indexed by natural numbers, the theorem guarantees the existence of a subsequence `g` that is either strictly increasing or not strictly increasing under the relation `r`. This means that for any pair of indices `m` and `n` where `m < n`, the value at the `m`-th position of the subsequence `g` is strictly related to the `n`-th position in `g` under `r`, or it is not strictly related under `r`. This theorem essentially asserts the existence of monotonic or non-monotonic subsequences for any given sequence.
More concisely: Given a type `α`, a transitive binary relation `r` on `α`, and a sequence `f` of elements from `α` indexed by natural numbers, there exists a subsequence `g` such that for all pairs of indices `m` and `n` where `m < n`, either `g(m) r g(n)` or `g(m) ∉ r g(n)`.
|
RelEmbedding.wellFounded_iff_no_descending_seq
theorem RelEmbedding.wellFounded_iff_no_descending_seq :
∀ {α : Type u_1} {r : α → α → Prop} [inst : IsStrictOrder α r],
WellFounded r ↔ IsEmpty ((fun x x_1 => x > x_1) ↪r r)
This theorem states that, for any type `α` and a relation `r` on `α` where `r` is a strict order, the relation `r` is well-founded if and only if there does not exist any infinite decreasing sequence. In other words, a relation is well-founded when it's impossible to find an infinite sequence where each element is strictly larger than the next according to the relation `r`. This means that for every nonempty subset, there is a minimal element with respect to the relation `r`.
More concisely: A relation on a type is well-founded if and only if there is no infinite decreasing sequence with respect to the relation.
|
WellFounded.monotone_chain_condition
theorem WellFounded.monotone_chain_condition :
∀ {α : Type u_1} [inst : PartialOrder α],
(WellFounded fun x x_1 => x > x_1) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m
This theorem, known as the "monotone chain condition", states that for any type `α` with a partial order, the well-foundedness of the "greater than" relation is equivalent to the following condition: for any strictly increasing sequence `a` of elements of `α` indexed by natural numbers, there exists a natural number `n` such that for all natural numbers `m` greater than or equal to `n`, the `m`-th element of the sequence `a` is the same as the `n`-th element. In mathematical terms, this condition states that any non-decreasing sequence of elements in `α` eventually becomes constant.
More concisely: The monotone chain condition in a partially ordered type `α` asserts that a well-founded "greater than" relation implies that every strictly increasing sequence has a minimal element.
|